The Community for Technology Leaders
2011 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (2009)
Timisoara, Romania
Sept. 26, 2009 to Sept. 29, 2009
ISBN: 978-0-7695-3964-5
pp: 10
ABSTRACT
Invariants with quantifiers are important for verification and static analysis of programsover arrays due to the unbounded nature of arrays. Such invariants can expressrelationships among array elements and properties involving array and scalar variablesof the loop.This talk presents how quantified loop invariants of programs over arrayscan be automatically inferred using a first order theorem prover,reducing the burden of annotating loops with complete invariants.Unlike all previously known methods, our method is ableto generate loop invariants containing quantifier alternations
INDEX TERMS
loop invariants, theorem proving, program verification
CITATION
Laura Kovacs, Andrei Voronkov, "Finding Loop Invariants for Programs over Arrays Using a Theorem Prover", 2011 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, vol. 00, no. , pp. 10, 2009, doi:10.1109/SYNASC.2009.66
78 ms
(Ver 3.3 (11022016))