Solving non-linear Horn clauses using a linear Horn clause solver

MaRDI QIDQ5015369zbMATH OpenFDO

Authors Bishoksan Kafle, John P. Gallagher, Pierre Ganty

Publication date 7 December 2021

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Horn clause solvers for program verification
• Solving Horn clauses on inductive data types without induction
• Proving correctness of imperative programs by linearizing constrained Horn clauses
• HoIce: an ICE-based non-linear Horn clause solver
• Solving non-linear arithmetic

Cites work

• An Improved Tight Closure Algorithm for Integer Octagonal Constraints
• An overview of Ciao and its design philosophy
• Convergence of Newton's method over commutative semirings
• Fast offline partial evaluation of logic programs
• Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
• scientific article; zbMATH DE number 236855 (Why is no real title available?)
• Linearisability on Datalog programs
• On Fixed Point Equations over Commutative Semirings
• Parikh's theorem: a simple and direct automaton construction
• Proving correctness of imperative programs by linearizing constrained Horn clauses
• Tools and algorithms for the construction and analysis of systems. 21st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11--18, 2015. Proceedings
• Transformation by interpreter specialisation
• Underapproximation of procedure summaries for integer programs

Cited in

(9)

• A linear algorithm for renaming a set of clauses as a Horn set
• Horn clause solvers for program verification
• Normalization of linear Horn clauses
• Solving Horn clauses on inductive data types without induction
• Tree dimension in verification of constrained Horn clauses
• Synchronizing constrained Horn clauses
• HoIce: an ICE-based non-linear Horn clause solver
• Solving constrained Horn clauses over algebraic data types
• Regular path clauses and their application in solving loops

Describes a project that uses

Uses Software

• PPL
• Eldarica
• LOGEN
• VeriMAP
• Yices
• Princess
• FLATA
• HSF

This page was built for publication: Solving non-linear Horn clauses using a linear Horn clause solver

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