Abstract
Recursion-free Horn-clause constraints have received much recent attention in the verification community. It extends Craig interpolation, and is proposed as a unifying formalism for expressing abstraction refinement. In abstraction refinement, it is often desirable to infer “simple” refinements, and researchers have studied techniques for inferring simple Craig interpolants. Drawing on the line of work, this paper presents a technique for inferring simple solutions to recursion-free Hornclause constraints. Our contribution is a constraint solving algorithm that lazily samples fragments of the given constraints whose solution spaces are used to form a simple solution for the whole. We have implemented a prototype of the constraint solving algorithm in a verification tool, and have confirmed that it is able to infer simple solutions that aid the verification process.
| Original language | English |
|---|---|
| Title of host publication | Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings |
| Publisher | Springer Verlag |
| Pages | 149-163 |
| Number of pages | 15 |
| Volume | 9035 |
| ISBN (Electronic) | 9783662466803 |
| DOIs | |
| Publication status | Published - 2015 |
| Externally published | Yes |
| Event | 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 - London, United Kingdom Duration: 2015 Apr 11 → 2015 Apr 18 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 9035 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Other
| Other | 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 |
|---|---|
| Country | United Kingdom |
| City | London |
| Period | 15/4/11 → 15/4/18 |
Fingerprint
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)
Cite this
Inferring simple solutions to recursion-free horn clauses via sampling. / Unno, Hiroshi; Terauchi, Tachio.
Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. Vol. 9035 Springer Verlag, 2015. p. 149-163 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9035).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
}
TY - GEN
T1 - Inferring simple solutions to recursion-free horn clauses via sampling
AU - Unno, Hiroshi
AU - Terauchi, Tachio
PY - 2015
Y1 - 2015
N2 - Recursion-free Horn-clause constraints have received much recent attention in the verification community. It extends Craig interpolation, and is proposed as a unifying formalism for expressing abstraction refinement. In abstraction refinement, it is often desirable to infer “simple” refinements, and researchers have studied techniques for inferring simple Craig interpolants. Drawing on the line of work, this paper presents a technique for inferring simple solutions to recursion-free Hornclause constraints. Our contribution is a constraint solving algorithm that lazily samples fragments of the given constraints whose solution spaces are used to form a simple solution for the whole. We have implemented a prototype of the constraint solving algorithm in a verification tool, and have confirmed that it is able to infer simple solutions that aid the verification process.
AB - Recursion-free Horn-clause constraints have received much recent attention in the verification community. It extends Craig interpolation, and is proposed as a unifying formalism for expressing abstraction refinement. In abstraction refinement, it is often desirable to infer “simple” refinements, and researchers have studied techniques for inferring simple Craig interpolants. Drawing on the line of work, this paper presents a technique for inferring simple solutions to recursion-free Hornclause constraints. Our contribution is a constraint solving algorithm that lazily samples fragments of the given constraints whose solution spaces are used to form a simple solution for the whole. We have implemented a prototype of the constraint solving algorithm in a verification tool, and have confirmed that it is able to infer simple solutions that aid the verification process.
UR - http://www.scopus.com/inward/record.url?scp=84926629327&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84926629327&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-46681-0_10
DO - 10.1007/978-3-662-46681-0_10
M3 - Conference contribution
AN - SCOPUS:84926629327
VL - 9035
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 149
EP - 163
BT - Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings
PB - Springer Verlag
ER -