Paper Info
Title
Smt-Based Array Invariant Generation
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 Larraz1573.44
Enric Rodríguez-Carbonell244626.13
Albert Rubio322819.44