Proving correctness of imperative programs by linearizing constrained Horn clauses

DOI10.1017/S1471068415000289zbMath1379.68093arXiv1507.05877MaRDI QIDQ4593003

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

Publication date: 9 November 2017

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1507.05877

zbMATH Keywords

Horn clausesprogram transformationconstraint logic programmingprogram verificationpartial correctness specifications

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (7)

Solving Horn Clauses on Inductive Data Types Without Induction ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Predicate Pairing for program verification ⋮ Tree dimension in verification of constrained Horn clauses ⋮ Abstract conjunctive partial deduction for the analysis and compilation of coroutines

Uses Software

• ECCE
• z3
• ARMC
• TRACER
• MathSAT5
• VeriMAP

Cites Work

• Unnamed Item
• Unnamed Item
• Transformations of CLP modules
• Verification of sequential and concurrent programs
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Generating all polynomial invariants in simple loops
• TRACER: A Symbolic Execution Tool for Verification
• REACHABILITY ANALYSIS IN VERIFICATION VIA SUPERCOMPILATION
• Theories of Programming Languages
• Conjunctive partial deduction: foundations, control, algorithms, and experiments
• Generalization strategies for the verification of infinite state systems
• The MathSAT5 SMT Solver
• An axiomatic basis for computer programming

This page was built for publication: Proving correctness of imperative programs by linearizing constrained Horn clauses