Proving consistency of pure methods and model fields

R. Leino; R. Middelkoop

doi:10.1007/978-3-642-00593-0_16

Proving consistency of pure methods and model fields

R. Leino, R. Middelkoop

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

3 Citations (Scopus)

Abstract

Pure methods and model fields are useful and common specification constructs that can be interpreted by the introduction of axioms in a program verifier’s underlying proof system. Care has to be taken that these axioms do not introduce an inconsistency into the proof system. This paper describes and proves sound an approach that ensures no inconsistencies are introduced. Unlike some previous syntax-based approaches, this approach is based on semantics, which lets it admit some natural but previously problematical specifications. The semantic conditions are discharged by the program verifier using an SMT solver, and the paper describes heuristics that help avoid common problems in finding witnesses with trigger-based SMT solvers. The paper reports on the positive experience with using this approach in Spec# for over a year.

Original language	English
Title of host publication	Fundamental Approaches to Software Engineering (12th International Conference, FASE'09, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings)
Editors	M. Chechik, M. Wirsing
Place of Publication	Berlin
Publisher	Springer
Pages	231-245
ISBN (Print)	978-3-642-00592-3
DOIs	https://doi.org/10.1007/978-3-642-00593-0_16
Publication status	Published - 2009

Publication series

Name	Lecture Notes in Computer Science
Volume	5503
ISSN (Print)	0302-9743

Access to Document

10.1007/978-3-642-00593-0_16

Cite this

Leino, R., & Middelkoop, R. (2009). Proving consistency of pure methods and model fields. In M. Chechik, & M. Wirsing (Eds.), Fundamental Approaches to Software Engineering (12th International Conference, FASE'09, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings) (pp. 231-245). (Lecture Notes in Computer Science; Vol. 5503). Springer. https://doi.org/10.1007/978-3-642-00593-0_16

Leino, R. ; Middelkoop, R. / Proving consistency of pure methods and model fields. Fundamental Approaches to Software Engineering (12th International Conference, FASE'09, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings). editor / M. Chechik ; M. Wirsing. Berlin : Springer, 2009. pp. 231-245 (Lecture Notes in Computer Science).

@inproceedings{d271a9b9597044cf8869b49bc0ce5c96,

title = "Proving consistency of pure methods and model fields",

abstract = "Pure methods and model fields are useful and common specification constructs that can be interpreted by the introduction of axioms in a program verifier{\textquoteright}s underlying proof system. Care has to be taken that these axioms do not introduce an inconsistency into the proof system. This paper describes and proves sound an approach that ensures no inconsistencies are introduced. Unlike some previous syntax-based approaches, this approach is based on semantics, which lets it admit some natural but previously problematical specifications. The semantic conditions are discharged by the program verifier using an SMT solver, and the paper describes heuristics that help avoid common problems in finding witnesses with trigger-based SMT solvers. The paper reports on the positive experience with using this approach in Spec# for over a year.",

author = "R. Leino and R. Middelkoop",

year = "2009",

doi = "10.1007/978-3-642-00593-0_16",

language = "English",

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

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "231--245",

editor = "M. Chechik and M. Wirsing",

booktitle = "Fundamental Approaches to Software Engineering (12th International Conference, FASE'09, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings)",

address = "Germany",

}

Leino, R & Middelkoop, R 2009, Proving consistency of pure methods and model fields. in M Chechik & M Wirsing (eds), Fundamental Approaches to Software Engineering (12th International Conference, FASE'09, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings). Lecture Notes in Computer Science, vol. 5503, Springer, Berlin, pp. 231-245. https://doi.org/10.1007/978-3-642-00593-0_16

Proving consistency of pure methods and model fields. / Leino, R.; Middelkoop, R.

Fundamental Approaches to Software Engineering (12th International Conference, FASE'09, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings). ed. / M. Chechik; M. Wirsing. Berlin : Springer, 2009. p. 231-245 (Lecture Notes in Computer Science; Vol. 5503).

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

TY - GEN

T1 - Proving consistency of pure methods and model fields

AU - Leino, R.

AU - Middelkoop, R.

PY - 2009

Y1 - 2009

N2 - Pure methods and model fields are useful and common specification constructs that can be interpreted by the introduction of axioms in a program verifier’s underlying proof system. Care has to be taken that these axioms do not introduce an inconsistency into the proof system. This paper describes and proves sound an approach that ensures no inconsistencies are introduced. Unlike some previous syntax-based approaches, this approach is based on semantics, which lets it admit some natural but previously problematical specifications. The semantic conditions are discharged by the program verifier using an SMT solver, and the paper describes heuristics that help avoid common problems in finding witnesses with trigger-based SMT solvers. The paper reports on the positive experience with using this approach in Spec# for over a year.

AB - Pure methods and model fields are useful and common specification constructs that can be interpreted by the introduction of axioms in a program verifier’s underlying proof system. Care has to be taken that these axioms do not introduce an inconsistency into the proof system. This paper describes and proves sound an approach that ensures no inconsistencies are introduced. Unlike some previous syntax-based approaches, this approach is based on semantics, which lets it admit some natural but previously problematical specifications. The semantic conditions are discharged by the program verifier using an SMT solver, and the paper describes heuristics that help avoid common problems in finding witnesses with trigger-based SMT solvers. The paper reports on the positive experience with using this approach in Spec# for over a year.

U2 - 10.1007/978-3-642-00593-0_16

DO - 10.1007/978-3-642-00593-0_16

M3 - Conference contribution

SN - 978-3-642-00592-3

T3 - Lecture Notes in Computer Science

SP - 231

EP - 245

BT - Fundamental Approaches to Software Engineering (12th International Conference, FASE'09, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings)

A2 - Chechik, M.

A2 - Wirsing, M.

PB - Springer

CY - Berlin

ER -

Leino R, Middelkoop R. Proving consistency of pure methods and model fields. In Chechik M, Wirsing M, editors, Fundamental Approaches to Software Engineering (12th International Conference, FASE'09, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings). Berlin: Springer. 2009. p. 231-245. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-00593-0_16

Proving consistency of pure methods and model fields

Abstract

Publication series

Access to Document

Fingerprint

Cite this