A case study on automation of verification logics

Reiner Dojen; Tom Coffey

doi:10.1109/INES.2005.1555146

A case study on automation of verification logics

Reiner Dojen, Tom Coffey

Department of Electronics & Computer Engineering

University of Limerick

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Formal logics are increasingly used to verify correctness of theories and designs in engineering. However, the process of logic-based verification is complex, tedious and prone to error. This is a serious issue, as a single mistake can render the result of the verification useless. Automated techniques reduce the potential for human errors during verification. This paper presents the theoretical concept of Layered Proving Trees, for the automation of logic-based verification. Verification tools based on Layered Proving Trees result in comparatively simple - but powerful - systems. Empirical result on the performance of a prototype implementation of a layered proving trees verification tool are presented.

Original language	English
Title of host publication	INES'05
Subtitle of host publication	IEEE 9th International Conference on Intelligent Engineering Systems - Proceedings
Publisher	IEEE Computer Society
Pages	139-144
Number of pages	6
ISBN (Print)	0780394747, 9780780394742
DOIs	https://doi.org/10.1109/INES.2005.1555146
Publication status	Published - 2005
Event	INES'05: IEEE 9th International Conference on Intelligent Engineering Systems - Duration: 16 Sep 2005 → 19 Sep 2005

Publication series

Name	INES'05: IEEE 9th International Conference on Intelligent Engineering Systems - Proceedings
Volume	2005

Conference

Conference	INES'05: IEEE 9th International Conference on Intelligent Engineering Systems
Period	16/09/05 → 19/09/05

Access to Document

10.1109/INES.2005.1555146

Cite this

Dojen, R., & Coffey, T. (2005). A case study on automation of verification logics. In INES'05: IEEE 9th International Conference on Intelligent Engineering Systems - Proceedings (pp. 139-144). Article 1555146 (INES'05: IEEE 9th International Conference on Intelligent Engineering Systems - Proceedings; Vol. 2005). IEEE Computer Society. https://doi.org/10.1109/INES.2005.1555146

@inproceedings{a09e45efca7740bca313806a2a6bc882,

title = "A case study on automation of verification logics",

abstract = "Formal logics are increasingly used to verify correctness of theories and designs in engineering. However, the process of logic-based verification is complex, tedious and prone to error. This is a serious issue, as a single mistake can render the result of the verification useless. Automated techniques reduce the potential for human errors during verification. This paper presents the theoretical concept of Layered Proving Trees, for the automation of logic-based verification. Verification tools based on Layered Proving Trees result in comparatively simple - but powerful - systems. Empirical result on the performance of a prototype implementation of a layered proving trees verification tool are presented.",

author = "Reiner Dojen and Tom Coffey",

year = "2005",

doi = "10.1109/INES.2005.1555146",

language = "English",

isbn = "0780394747",

series = "INES'05: IEEE 9th International Conference on Intelligent Engineering Systems - Proceedings",

publisher = "IEEE Computer Society",

pages = "139--144",

booktitle = "INES'05",

note = "INES'05: IEEE 9th International Conference on Intelligent Engineering Systems ; Conference date: 16-09-2005 Through 19-09-2005",

}

Dojen, R & Coffey, T 2005, A case study on automation of verification logics. in INES'05: IEEE 9th International Conference on Intelligent Engineering Systems - Proceedings., 1555146, INES'05: IEEE 9th International Conference on Intelligent Engineering Systems - Proceedings, vol. 2005, IEEE Computer Society, pp. 139-144, INES'05: IEEE 9th International Conference on Intelligent Engineering Systems, 16/09/05. https://doi.org/10.1109/INES.2005.1555146

A case study on automation of verification logics. / Dojen, Reiner; Coffey, Tom.
INES'05: IEEE 9th International Conference on Intelligent Engineering Systems - Proceedings. IEEE Computer Society, 2005. p. 139-144 1555146 (INES'05: IEEE 9th International Conference on Intelligent Engineering Systems - Proceedings; Vol. 2005).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A case study on automation of verification logics

AU - Dojen, Reiner

AU - Coffey, Tom

PY - 2005

Y1 - 2005

N2 - Formal logics are increasingly used to verify correctness of theories and designs in engineering. However, the process of logic-based verification is complex, tedious and prone to error. This is a serious issue, as a single mistake can render the result of the verification useless. Automated techniques reduce the potential for human errors during verification. This paper presents the theoretical concept of Layered Proving Trees, for the automation of logic-based verification. Verification tools based on Layered Proving Trees result in comparatively simple - but powerful - systems. Empirical result on the performance of a prototype implementation of a layered proving trees verification tool are presented.

AB - Formal logics are increasingly used to verify correctness of theories and designs in engineering. However, the process of logic-based verification is complex, tedious and prone to error. This is a serious issue, as a single mistake can render the result of the verification useless. Automated techniques reduce the potential for human errors during verification. This paper presents the theoretical concept of Layered Proving Trees, for the automation of logic-based verification. Verification tools based on Layered Proving Trees result in comparatively simple - but powerful - systems. Empirical result on the performance of a prototype implementation of a layered proving trees verification tool are presented.

UR - http://www.scopus.com/inward/record.url?scp=33845477651&partnerID=8YFLogxK

U2 - 10.1109/INES.2005.1555146

DO - 10.1109/INES.2005.1555146

M3 - Conference contribution

AN - SCOPUS:33845477651

SN - 0780394747

SN - 9780780394742

T3 - INES'05: IEEE 9th International Conference on Intelligent Engineering Systems - Proceedings

SP - 139

EP - 144

BT - INES'05

PB - IEEE Computer Society

T2 - INES'05: IEEE 9th International Conference on Intelligent Engineering Systems

Y2 - 16 September 2005 through 19 September 2005

ER -

A case study on automation of verification logics

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this