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. |
Year | DOI | Venue |
---|---|---|
2013 | 10.1007/978-3-642-35873-9_12 | VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION (VMCAI 2013) |
Keywords | Field | DocType |
Program correctness, Invariant generation, SMT | Computer science,Scalar (physics),Theoretical computer science,Loop invariant,Invariant (mathematics),Spectrum analyzer,Satisfiability modulo theories | Conference |
Volume | ISSN | Citations |
7737 | 0302-9743 | 16 |
PageRank | References | Authors |
0.62 | 22 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Daniel Larraz | 1 | 57 | 3.44 |
Enric Rodríguez-Carbonell | 2 | 446 | 26.13 |
Albert Rubio | 3 | 228 | 19.44 |