Loading...
Please wait, while we are loading the content...
On Set-Driven Combination of Logics and Verifiers
| Content Provider | Semantic Scholar |
|---|---|
| Author | Kuncak, Viktor Wies, Thomas |
| Copyright Year | 2009 |
| Abstract | We explore the problem of automated reasoning about the non-disjoint combination of logics that share set variables and operations. We prove a general combination theorem, and apply it to show the decidability for the quantifier-free combination of formulas in WS2S, two-varible logic with counting, and Boolean Algebra with Presburger Arithmetic. Furthermore, we present an over-approximating algorithm that uses such combined logics to synthesize universally quantified invariants of infinite-state systems. The algorithm simultaneously synthesizes loop invariants of interest, and infers the relationships between sets to exchange the information between logics. We have implemented this algorithm and used it to prove detailed correctness properties of operations of linked data structure implementations. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://lara.epfl.ch/~kuncak/papers/KuncakWies09SetDrivenCombinationofLogicsandVerifiers.pdf |
| Alternate Webpage(s) | http://mtc.epfl.ch/~wies/papers/KuncakWies09SetDrivenCombination.pdf |
| Alternate Webpage(s) | http://pub.ist.ac.at/~wies/papers/KuncakWies09SetDrivenCombination.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
