Generalised interpolation by solving recursion-free Horn clauses

MaRDI QIDQ4997234zbMATH OpenFDO

Authors Ashutosh Gupta, Andrey Rybalchenko, C. Popeea

Publication date 28 June 2021

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40)

Recommendations

• On recursion-free Horn clauses and Craig interpolation
• Inferring simple solutions to recursion-free Horn clauses via sampling
• Constraint Solving for Interpolation
• Constraint solving for interpolation
• Horn clause solvers for program verification

Cited in

(10)

• Inferring simple solutions to recursion-free Horn clauses via sampling
• Iterative Specialisation of Horn Clauses
• Labelled interpolation systems for hyper-resolution, clausal, and local proofs
• HoIce: an ICE-based non-linear Horn clause solver
• Horn clause solvers for program verification
• On recursion-free Horn clauses and Craig interpolation
• A fixed-point theorem for Horn formula equations
• An abstract fixed-point theorem for Horn formula equations
• Efficient Generation of Small Interpolants in CNF
• On Interpolation and Automatization for Frege Systems

This page was built for publication: Generalised interpolation by solving recursion-free Horn clauses

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