Exploiting partial variable assignment in interpolation-based model checking
| Autor: | Antti E. J. Hyvärinen, Jan Kofroň, Leonardo Alt, Grigory Fedyukovich, Natasha Sharygina, Pavel Jančík |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Model checking
Computer science Computation MathematicsofComputing_NUMERICALANALYSIS 02 engineering and technology Extension (predicate logic) 020202 computer hardware & architecture Theoretical Computer Science Set (abstract data type) Variable (computer science) Hardware and Architecture ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Algorithm Software ComputingMethodologies_COMPUTERGRAPHICS Abstraction (linguistics) Interpolation |
| Zdroj: | Formal Methods in System Design. 55:33-71 |
| ISSN: | 1572-8102 0925-9856 |
| DOI: | 10.1007/s10703-019-00342-z |
| Popis: | Craig interpolation has been successfully employed in symbolic program verification as a means of abstraction for sets of program states. In this article, we present the partial variable assignment interpolation system, an extension of the labeled interpolation system, enriched by partial variable assignments. It allows for both generation of smaller interpolants as well as for their faster computation. We present proofs of important properties of the interpolation system as well as a set of experiments proving its usefulness. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink