A FOOLish encoding of the next state relations of imperative programs

DOI10.1007/978-3-319-94205-6_27MaRDI QIDQ1799102zbMATH OpenOpenAlexFDO

Authors E. A. Kotel'nikov, Laura Kovács, Andrei Voronkov

Publication date 18 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-94205-6_27

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• A formalization of programs in first-order logic with a discrete linear order
• On automated program construction and verification
• Characteristic formulae for the verification of imperative programs
• Theories for mechanical proofs of imperative programs

Cited in

(2)

• The Shadow Knows: Refinement of Ignorance in Sequential Programs
• A Polymorphic Vampire

Describes a project that uses

Uses Software

• SMT-LIB
• StarExec
• Boogie
• VAMPIRE
• Why3
• z3
• TPTP

This page was built for publication: A FOOLish encoding of the next state relations of imperative programs

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