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

DOI10.1007/978-3-319-21690-4_4MaRDI QIDQ1702910zbMATH OpenOpenAlexFDO

Authors Daniel Dietsch, Matthias Heizmann, Vincent Langenfeld, Andreas Podelski

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

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

Recommendations

• Model Checking Almost All Paths Can Be Less Expensive Than Checking All Paths
• Model checking with strong fairness
• \(\mathrm{LTL}_{f}\) satisfiability checking
• Modalities for model checking: Branching time logic strikes back
• Model checking LTLR formulas under localized fairness

Cited in

(7)

• Translating Xd-C programs to MSVL programs
• scientific article; zbMATH DE number 1755146 (Why is no real title available?)
• Temporal prophecy for proving temporal properties of infinite-state systems
• A compiler for MSVL and its applications
• Temporal verification of programs via first-order fixpoint logic
• Fold/unfold transformations for fixpoint logic
• Verifying a scheduling protocol of safety-critical systems

Describes a project that uses

Uses Software

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

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

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