Loading...
Please wait, while we are loading the content...
Similar Documents
Proving correctness of imperative programs by linearizing constrained Horn clauses
| Content Provider | Scilit |
|---|---|
| Author | Angelis, Emanuele D. E. Fioravanti, Fabio Pettorossi, Alberto Proietti, Maurizio |
| Copyright Year | 2015 |
| Description | We present a method for verifying the correctness of imperative programs which is based on the automated transformation of their specifications. Given a programprog, we consider a partial correctness specification of the form {ϕ},prog{ψ}, where the assertions ϕ and ψ are predicates defined by a setSpecof possibly recursive Horn clauses with linear arithmetic (LA) constraints in their premise (also calledconstrained Horn clauses). The verification method consists in constructing a setPCof constrained Horn clauses whose satisfiability implies that {ϕ},prog, {ψ} is valid. We highlight some limitations of state-of-the-art constrained Horn clause solving methods, here calledLA-solving methods, which prove the satisfiability of the clauses by looking for linear arithmetic interpretations of the predicates. In particular, we prove that there exist some specifications that cannot be proved valid by any of thoseLA-solving methods. These specifications require the proof of satisfiability of a setPCof constrained Horn clauses that containnonlinear clauses(that is, clauses with more than one atom in their premise). Then, we present a transformation, calledlinearization, that convertsPCinto a set oflinearclauses (that is, clauses with at most one atom in their premise). We show that several specifications that could not be proved valid byLA-solving methods, can be proved valid after linearization. We also present a strategy for performing linearization in an automatic way and we report on some experimental results obtained by using a preliminary implementation of our method. |
| Related Links | http://arxiv.org/pdf/1507.05877 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/A2112FBF4E90BACD00E0A8EC0F0FBA9F/S1471068415000289a.pdf/div-class-title-proving-correctness-of-imperative-programs-by-linearizing-constrained-horn-clauses-div.pdf |
| Ending Page | 650 |
| Page Count | 16 |
| Starting Page | 635 |
| ISSN | 14710684 |
| e-ISSN | 14753081 |
| DOI | 10.1017/s1471068415000289 |
| Journal | Theory and Practice of Logic Programming |
| Issue Number | 4-5 |
| Volume Number | 15 |
| Language | English |
| Publisher | Cambridge University Press (CUP) |
| Publisher Date | 2015-07-01 |
| Access Restriction | Open |
| Subject Keyword | Theory and Practice of Logic Programming Program Verification Partial Correctness Specifications Horn Clauses Constraint Logic Programming Program Transformation |
| Content Type | Text |
| Resource Type | Article |
| Subject | Artificial Intelligence Theoretical Computer Science Computational Theory and Mathematics Hardware and Architecture Software |
