|
| | | | |
| | | |
| Stat |
Members: 3645
Articles: 2'506'133
Articles rated: 2609
27 April 2024 |
|
| | | | |
|
Article overview
| |
|
|
Verification of Programs by Combining Iterated Specialization with Interpolation | | Emanuele De Angelis
; Fabio Fioravanti
; Jorge A. Navas
; Maurizio Proietti
; | | Date: |
3 Dec 2014 | | Abstract: | We present a verification technique for program safety that combines Iterated
Specialization and Interpolating Horn Clause Solving. Our new method composes
together these two techniques in a modular way by exploiting the common Horn
Clause representation of the verification problem. The Iterated Specialization
verifier transforms an initial set of verification conditions by using
unfold/fold equivalence preserving transformation rules. During transformation,
program invariants are discovered by applying widening operators. Then the
output set of specialized verification conditions is analyzed by an
Interpolating Horn Clause solver, hence adding the effect of interpolation to
the effect of widening. The specialization and interpolation phases can be
iterated, and also combined with other transformations that change the
direction of propagation of the constraints (forward from the program
preconditions or backward from the error conditions). We have implemented our
verification technique by integrating the VeriMAP verifier with the FTCLP Horn
Clause solver, based on Iterated Specialization and Interpolation,
respectively. Our experimental results show that the integrated verifier
improves the precision of each of the individual components run separately. | | Source: | arXiv, 1412.1151 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser Mozilla/5.0 AppleWebKit/537.36 (KHTML, like Gecko; compatible; ClaudeBot/1.0; +claudebot@anthropic.com)
|
| |
|
|
|
|
News, job offers and information for researchers and scientists:
| |
REGISTER