A FOOLish encoding of the next state relations of imperative programs

DOI10.1007/978-3-319-94205-6_27OpenAlexW2802944976MaRDI QIDQ1799102

Evgenii Kotelnikov, Andrei Voronkov, Laura Kovács

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

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

Related Items (1)

A Polymorphic Vampire

Uses Software

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

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