|
| | | | |
| | | |
| Stat |
Members: 3645
Articles: 2'503'724
Articles rated: 2609
23 April 2024 |
|
| | | | |
|
Article overview
| |
|
|
Predicate Pairing for Program Verification | | Emanuele De Angelis
; Fabio Fioravanti
; Alberto Pettorossi
; Maurizio Proietti
; | | Date: |
4 Aug 2017 | | Abstract: | It is well-known that the verification of partial correctness properties of
imperative programs can be reduced to the satisfiability problem for
constrained Horn clauses (CHCs). However, state-of-the-art solvers for CHCs
(CHC solvers) based on predicate abstraction are sometimes unable to verify
satisfiability because they look for models that are definable in a given class
A of constraints, called A-definable models. We introduce a transformation
technique, called Predicate Pairing (PP), which is able, in many interesting
cases, to transform a set of clauses into an equisatisfiable set whose
satisfiability can be proved by finding an A-definable model, and hence can be
effectively verified by CHC solvers. We prove that, under very general
conditions on A, the unfold/fold transformation rules preserve the existence of
an A-definable model, i.e., if the original clauses have an A-definable model,
then the transformed clauses have an A-definable model. The converse does not
hold in general, and we provide suitable conditions under which the transformed
clauses have an A-definable model iff the original ones have an A-definable
model. Then, we present the PP strategy which guides the application of the
transformation rules with the objective of deriving a set of clauses whose
satisfiability can be proved by looking for A-definable models. PP introduces a
new predicate defined by the conjunction of two predicates together with some
constraints. We show through some examples that an A-definable model may exist
for the new predicate even if it does not exist for its defining atomic
conjuncts. We also present some case studies showing that PP plays a crucial
role in the verification of relational properties of programs (e.g., program
equivalence and non-interference). Finally, we perform an experimental
evaluation to assess the effectiveness of PP in increasing the power of CHC
solving. | | Source: | arXiv, 1708.1473 | | 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