Verification of Imperative Programs by Constraint Logic Program Transformation
We present a method for verifying partial correctness properties of imperative programs that manipulate integers and arrays by using techniques based on the transformation of constraint logic programs (CLP). We use CLP as a metalanguage for representing imperative programs, their executions, and the...
Main Authors: | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2013-09-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1309.5139v1 |
Similar Items
-
Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification
by: Emanuele De Angelis, et al.
Published: (2019-07-01) -
Removing Unnecessary Variables from Horn Clause Verification Conditions
by: Emanuele De Angelis, et al.
Published: (2016-07-01) -
Towards certified program logics for the verification of imperative programs
by: David Miguel Ramalho Pereira
Published: (2019) -
Logic programming tools and techniques for imperative program verification
by: O'Neill, I. M.
Published: (1987) -
Verification of Programs by Combining Iterated Specialization with Interpolation
by: Emanuele De Angelis, et al.
Published: (2014-12-01)