TY - GEN
T1 - Inferring simple solutions to recursion-free horn clauses via sampling
AU - Unno, Hiroshi
AU - Terauchi, Tachio
PY - 2015/1/1
Y1 - 2015/1/1
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
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
A2 - Tinelli, Cesare
A2 - Baier, Christel
PB - Springer Verlag
T2 - 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
Y2 - 11 April 2015 through 18 April 2015
ER -