Verification of imperative programs by constraint logic program transformation

MaRDI QIDQ4994693zbMATH OpenFDO

Authors Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti

Publication date 21 June 2021

Full work available at URL https://arxiv.org/abs/1309.5139, http://eptcs.web.cse.unsw.edu.au/paper.cgi?DSS2013.12

Mathematics Subject Classification ID

Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Program verification using constraint handling rules and array constraint generalizations
• Verifying Array Programs by Transforming Verification Conditions
• A rule-based verification strategy for array manipulating programs
• Proving correctness of imperative programs by linearizing constrained Horn clauses
• Logic programs as specifications in the inductive verification of logic programs

Cited in

(9)

• Kima: An automated error correction system for concurrent logic programs
• Specialization with constrained generalization for software model checking
• A rule-based verification strategy for array manipulating programs
• A Transformational Approach for Proving Properties of the CHR Constraint Store
• scientific article; zbMATH DE number 1538039 (Why is no real title available?)
• Program verification using constraint handling rules and array constraint generalizations
• Proving correctness of imperative programs by linearizing constrained Horn clauses
• Characteristic formulae for the verification of imperative programs
• Verifying procedural programs via constrained rewriting induction

This page was built for publication: Verification of imperative programs by constraint logic program transformation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4994693)