Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-17164-2_23
Title: Automatically inferring quantified loop invariants by algorithmic learning from simple templates
Authors: Kong, S.
Jung, Y.
David, C. 
Wang, B.-Y.
Yi, K.
Issue Date: 2010
Citation: Kong, S.,Jung, Y.,David, C.,Wang, B.-Y.,Yi, K. (2010). Automatically inferring quantified loop invariants by algorithmic learning from simple templates. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6461 LNCS : 328-343. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-17164-2_23
Abstract: By combining algorithmic learning, decision procedures, predicate abstraction, and simple templates, we present an automated technique for finding quantified loop invariants. Our technique can find arbitrary first-order invariants (modulo a fixed set of atomic propositions and an underlying SMT solver) in the form of the given template and exploits the flexibility in invariants by a simple randomized mechanism. The proposed technique is able to find quantified invariants for loops from the Linux source, as well as for the benchmark code used in the previous works. Our contribution is a simpler technique than the previous works yet with a reasonable derivation power. © 2010 Springer-Verlag.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/124984
ISBN: 364217163X
ISSN: 03029743
DOI: 10.1007/978-3-642-17164-2_23
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.