Program verification using constraint handling rules and array constraint generalizations

DOI10.3233/FI-2017-1461zbMATH Open1374.68113MaRDI QIDQ4589602FDOQ4589602

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

Publication date: 10 November 2017

Published in: Fundamenta Informaticae (Search for Journal in Brave)

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

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)

Cited In (8)

• Title not available (Why is that?)
• 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
• Solving Horn Clauses on Inductive Data Types Without 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

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)