Program verification using constraint handling rules and array constraint generalizations

DOI10.3233/FI-2017-1461MaRDI QIDQ4589602zbMATH OpenFDO

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

Publication date 10 November 2017

Published in Fundamenta Informaticae (Search for Journal in Brave)

zbMATH Keywords

constraint logic programmingprogram verificationprogram transformationconstraint handling rules

Mathematics Subject Classification ID

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

Recommendations

• Verification of imperative programs by constraint logic program transformation
• A rule-based verification strategy for array manipulating programs
• Verifying Array Programs by Transforming Verification Conditions
• Verifying procedural programs via constrained rewriting induction
• Proving correctness of imperative programs by linearizing constrained Horn clauses

Cited in

(12)

• scientific article; zbMATH DE number 7447758 (Why is no real title available?)
• Automatic constrained rewriting induction towards verifying procedural programs
• Verification of imperative programs by constraint logic program transformation
• Generalised multi-pattern-based verification of programs with linear linked structures
• Reasoning in the theory of heap: satisfiability and interpolation
• Verifying Array Programs by Transforming Verification Conditions
• Verifying procedural programs via constrained rewriting induction
• Tools and Algorithms for the Construction and Analysis of Systems
• CPBPV: a constraint-programming framework for bounded program verification
• Putting the squeeze on array programs: loop verification via inductive rank reduction
• Solving Horn clauses on inductive data types without induction
• A rule-based verification strategy for array manipulating programs

This page was built for publication: Program verification using constraint handling rules and array constraint generalizations

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