Abstract
This paper presents a constraint-based method for generating universally quantified loop invariants over array and scalar variables. Constraints are solved by means of an SMT solver, thus leveraging recent advances in SMT solving for the theory of non-linear arithmetic. The method has been implemented in a prototype program analyzer, and a wide sample of examples illustrating its power is shown. © Springer-Verlag 2013.
Author supplied keywords
Cite
CITATION STYLE
Larraz, D., Rodríguez-Carbonell, E., & Rubio, A. (2013). SMT-based array invariant generation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7737 LNCS, pp. 169–188). Springer Verlag. https://doi.org/10.1007/978-3-642-35873-9_12
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
