Horn clauses and constraints are very popular formalisms for specifying and verifying properties of programs written in a variety of programming languages, including imperative, functional, object-oriented, and concurrent languages. We briefly present an approach to the verification of imperative programs based on transformations of Horn clauses with constraints, also called Constrained Horn Clauses. The approach is to a large extent parametric with respect to the programming language and allows us to exploit the very effective techniques and tools that have been developed in the fields of logic programming and constraint solving.
Horn Clause Transformation for Program Verification
E De Angelis;F Fioravanti;A Pettorossi;M Proietti
2016
Abstract
Horn clauses and constraints are very popular formalisms for specifying and verifying properties of programs written in a variety of programming languages, including imperative, functional, object-oriented, and concurrent languages. We briefly present an approach to the verification of imperative programs based on transformations of Horn clauses with constraints, also called Constrained Horn Clauses. The approach is to a large extent parametric with respect to the programming language and allows us to exploit the very effective techniques and tools that have been developed in the fields of logic programming and constraint solving.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
