Auditing User-Provided Axioms in Software Verification Conditions

Paul Jackson; Florian Schanda; Angela Wallenburg

doi:10.1007/978-3-642-41010-9_11

Auditing User-Provided Axioms in Software Verification Conditions

Paul Jackson, Florian Schanda, Angela Wallenburg

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

Abstract

A common approach to formally checking assertions inserted into a program is to first generate verification conditions, logical sentences that, if then proven, ensure the assertions are correct. Sometimes users provide axioms that get incorporated into verification conditions. Such axioms can capture aspects of the program’s specification or can be hints to help automatic provers. There is always the danger of mistakes in these axioms. In the worst case these mistakes introduce inconsistencies and verification conditions become erroneously provable.

We discuss here our use of an SMT solver to investigate the quality of user-provided axioms, to check for inconsistencies in axioms and to verify expected relationships between axioms, for example.

Original language	English
Title of host publication	Formal Methods for Industrial Critical Systems
Subtitle of host publication	18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013. Proceedings
Editors	Charles Pecheur, Michael Dierkes
Publisher	Springer
Pages	154-168
Number of pages	15
Volume	8187
ISBN (Electronic)	978-3-642-41010-9
ISBN (Print)	978-3-642-41009-3
DOIs	https://doi.org/10.1007/978-3-642-41010-9_11
Publication status	Published - 2013

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	8187

Access to Document

10.1007/978-3-642-41010-9_11

Jackson Schanda ET AL 2013 Auditing User Provided Axioms in software verification conditionsAccepted author manuscript, 156 KB

http://dx.doi.org/10.1007/978-3-642-41010-9_11

Cite this

Jackson, P., Schanda, F., & Wallenburg, A. (2013). Auditing User-Provided Axioms in Software Verification Conditions. In C. Pecheur, & M. Dierkes (Eds.), Formal Methods for Industrial Critical Systems: 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013. Proceedings (Vol. 8187, pp. 154-168). (Lecture Notes in Computer Science; Vol. 8187). Springer. https://doi.org/10.1007/978-3-642-41010-9_11

Jackson, Paul ; Schanda, Florian ; Wallenburg, Angela. / Auditing User-Provided Axioms in Software Verification Conditions. Formal Methods for Industrial Critical Systems: 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013. Proceedings. editor / Charles Pecheur ; Michael Dierkes. Vol. 8187 Springer, 2013. pp. 154-168 (Lecture Notes in Computer Science).

@inproceedings{dca9190736004aa8967cc5f6e26b06cc,

title = "Auditing User-Provided Axioms in Software Verification Conditions",

abstract = "A common approach to formally checking assertions inserted into a program is to first generate verification conditions, logical sentences that, if then proven, ensure the assertions are correct. Sometimes users provide axioms that get incorporated into verification conditions. Such axioms can capture aspects of the program{\textquoteright}s specification or can be hints to help automatic provers. There is always the danger of mistakes in these axioms. In the worst case these mistakes introduce inconsistencies and verification conditions become erroneously provable.We discuss here our use of an SMT solver to investigate the quality of user-provided axioms, to check for inconsistencies in axioms and to verify expected relationships between axioms, for example.",

author = "Paul Jackson and Florian Schanda and Angela Wallenburg",

year = "2013",

doi = "10.1007/978-3-642-41010-9_11",

language = "English",

isbn = "978-3-642-41009-3",

volume = "8187",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "154--168",

editor = "Charles Pecheur and Michael Dierkes",

booktitle = "Formal Methods for Industrial Critical Systems",

address = "United Kingdom",

}

Jackson, P, Schanda, F & Wallenburg, A 2013, Auditing User-Provided Axioms in Software Verification Conditions. in C Pecheur & M Dierkes (eds), Formal Methods for Industrial Critical Systems: 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013. Proceedings. vol. 8187, Lecture Notes in Computer Science, vol. 8187, Springer, pp. 154-168. https://doi.org/10.1007/978-3-642-41010-9_11

Auditing User-Provided Axioms in Software Verification Conditions. / Jackson, Paul; Schanda, Florian; Wallenburg, Angela.
Formal Methods for Industrial Critical Systems: 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013. Proceedings. ed. / Charles Pecheur; Michael Dierkes. Vol. 8187 Springer, 2013. p. 154-168 (Lecture Notes in Computer Science; Vol. 8187).

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

TY - GEN

T1 - Auditing User-Provided Axioms in Software Verification Conditions

AU - Jackson, Paul

AU - Schanda, Florian

AU - Wallenburg, Angela

PY - 2013

Y1 - 2013

N2 - A common approach to formally checking assertions inserted into a program is to first generate verification conditions, logical sentences that, if then proven, ensure the assertions are correct. Sometimes users provide axioms that get incorporated into verification conditions. Such axioms can capture aspects of the program’s specification or can be hints to help automatic provers. There is always the danger of mistakes in these axioms. In the worst case these mistakes introduce inconsistencies and verification conditions become erroneously provable.We discuss here our use of an SMT solver to investigate the quality of user-provided axioms, to check for inconsistencies in axioms and to verify expected relationships between axioms, for example.

AB - A common approach to formally checking assertions inserted into a program is to first generate verification conditions, logical sentences that, if then proven, ensure the assertions are correct. Sometimes users provide axioms that get incorporated into verification conditions. Such axioms can capture aspects of the program’s specification or can be hints to help automatic provers. There is always the danger of mistakes in these axioms. In the worst case these mistakes introduce inconsistencies and verification conditions become erroneously provable.We discuss here our use of an SMT solver to investigate the quality of user-provided axioms, to check for inconsistencies in axioms and to verify expected relationships between axioms, for example.

U2 - 10.1007/978-3-642-41010-9_11

DO - 10.1007/978-3-642-41010-9_11

M3 - Conference contribution

SN - 978-3-642-41009-3

VL - 8187

T3 - Lecture Notes in Computer Science

SP - 154

EP - 168

BT - Formal Methods for Industrial Critical Systems

A2 - Pecheur, Charles

A2 - Dierkes, Michael

PB - Springer

ER -

Jackson P, Schanda F, Wallenburg A. Auditing User-Provided Axioms in Software Verification Conditions. In Pecheur C, Dierkes M, editors, Formal Methods for Industrial Critical Systems: 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013. Proceedings. Vol. 8187. Springer. 2013. p. 154-168. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-41010-9_11

Auditing User-Provided Axioms in Software Verification Conditions

Abstract

Publication series

Access to Document

Fingerprint

Cite this