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)

Full work available at URL https://doi.org/10.3233/FI-2017-1461

zbMATH Keywords

constraint handling rulesconstraint logic programmingprogram transformationprogram verification

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

(13)

• Reasoning in the theory of heap: satisfiability and interpolation
• Generalised multi-pattern-based verification of programs with linear linked structures
• Automatic constrained rewriting induction towards verifying procedural programs
• Verifying Array Programs by Transforming Verification Conditions
• A rule-based verification strategy for array manipulating programs
• Bounded symbolic execution for runtime error detection of Erlang programs
• Solving Horn clauses on inductive data types without induction
• Verification of imperative programs by constraint logic program transformation
• Verifying procedural programs via constrained rewriting induction
• Tools and Algorithms for the Construction and Analysis of Systems
• Runtime repeated recursion unfolding in CHR: a just-in-time online program optimization strategy that can achieve super-linear speedup
• Putting the squeeze on array programs: loop verification via inductive rank reduction
• CPBPV: a constraint-programming framework for bounded program verification

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)