Cell morphing: from array programs to array-free Horn clauses

DOI10.1007/978-3-662-53413-7_18zbMath1394.68081OpenAlexW2340697544MaRDI QIDQ1664399

David Monniaux, Laure Gonnord

Publication date: 27 August 2018

Full work available at URL: https://doi.org/10.1007/978-3-662-53413-7_18

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (7)

Verifying Array Manipulating Programs with Full-Program Induction ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ \textsc{Diffy}: inductive reasoning of array programs using difference invariants ⋮ Data abstraction: a general framework to handle program verification of data structures ⋮ Synthesizing history and prophecy variables for symbolic model checking ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays ⋮ Reasoning in the theory of heap: satisfiability and interpolation

This page was built for publication: Cell morphing: from array programs to array-free Horn clauses