PeRIPLO: a framework for producing effective interpolants in SAT-based software verification

DOI10.1007/978-3-642-45221-5_45MaRDI QIDQ2870162zbMATH OpenOpenAlexFDO

Authors Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina

Publication date 17 January 2014

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-45221-5_45

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Interpolation Properties and SAT-Based Model Checking
• Interpolation and SAT-based model checking.
• Constraint solving for interpolation
• Computer Science Logic
• Constraint Solving for Interpolation

Cited in

(9)

• Lattice-based refinement in bounded model checking
• Exploiting partial variable assignment in interpolation-based model checking
• Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys
• OpenSMT2: an SMT solver for multi-core and cloud computing
• Labelled interpolation systems for hyper-resolution, clausal, and local proofs
• Guiding Craig interpolation with domain-specific abstractions
• SMT-based verification of program changes through summary repair
• The \textsc{Golem} Horn solver
• \textsc{Golem}: a flexible and efficient solver for constrained Horn clauses

Describes a project that uses

Uses Software

• FunFrog
• PeRIPLO
• eVolCheck

This page was built for publication: PeRIPLO: a framework for producing effective interpolants in SAT-based software verification

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