TY - GEN
T1 - Separation predicates
T2 - 14th International Conference on Formal Engineering Methods, ICFEM 2012
AU - Bobot, François
AU - Filliâtre, Jean Christophe
PY - 2012/12/1
Y1 - 2012/12/1
N2 - This paper introduces separation predicates, a technique to reuse some ideas from separation logic in the framework of program verification using a traditional first-order logic. The purpose is to benefit from existing specification languages, verification condition generators, and automated theorem provers. Separation predicates are automatically derived from user-defined inductive predicates. We illustrate this idea on a non-trivial case study, namely the composite pattern, which is specified in C/ACSL and verified in a fully automatic way using SMT solvers Alt-Ergo, CVC3, and Z3.
AB - This paper introduces separation predicates, a technique to reuse some ideas from separation logic in the framework of program verification using a traditional first-order logic. The purpose is to benefit from existing specification languages, verification condition generators, and automated theorem provers. Separation predicates are automatically derived from user-defined inductive predicates. We illustrate this idea on a non-trivial case study, namely the composite pattern, which is specified in C/ACSL and verified in a fully automatic way using SMT solvers Alt-Ergo, CVC3, and Z3.
U2 - 10.1007/978-3-642-34281-3_14
DO - 10.1007/978-3-642-34281-3_14
M3 - Conference contribution
AN - SCOPUS:84871656101
SN - 9783642342806
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 167
EP - 181
BT - Formal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods, ICFEM 2012, Proceedings
Y2 - 12 November 2012 through 16 November 2012
ER -