Removing unnecessary variables from Horn clause verification conditions

MaRDI QIDQ5015370zbMATH OpenFDO

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

Publication date 7 December 2021

Full work available at URL https://arxiv.org/abs/1607.04460, http://eptcs.web.cse.unsw.edu.au/paper.cgi?HCVS2016.5

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Horn clause solvers for program verification
• Relational verification through Horn clause transformation
• Probabilistic Horn clause verification
• Solving Horn clauses on inductive data types without induction
• Proving correctness of imperative programs by linearizing constrained Horn clauses

Cites work

• Transformations of CLP modules
• Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs

Cited in

(1)

• Explaining Verification Conditions

Describes a project that uses

Uses Software

• z3
• SeaHorn
• VeriMAP

This page was built for publication: Removing unnecessary variables from Horn clause verification conditions

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