Fairness modulo theory: a new approach to LTL software model checking

DOI10.1007/978-3-319-21690-4_4zbMath1381.68157OpenAlexW1209505024MaRDI QIDQ1702910

Daniel Dietsch, Vincent Langenfeld, Andreas Podelski, Matthias Heizmann

Publication date: 1 March 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-21690-4_4

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (5)

A compiler for MSVL and its applications ⋮ Verifying a scheduling protocol of safety-critical systems ⋮ Fold/Unfold Transformations for Fixpoint Logic ⋮ Translating Xd-C programs to MSVL programs ⋮ Temporal prophecy for proving temporal properties of infinite-state systems

Uses Software

• SPIN
• DiVinE
• NuSMV
• ACSL
• SMTInterpol
• CPAchecker
• Bandera
• Cadence SMV
• AProVE
• OpenSMT
• SPOT
• MathSAT5
• CBMC
• Ultimate
• LTLAutomizer
• Ultimate Kojak
• FuncTion

This page was built for publication: Fairness modulo theory: a new approach to LTL software model checking