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

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

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

(11)

• A compiler for MSVL and its applications
• Temporal prophecy for proving temporal properties of infinite-state systems
• \textsc{LTL} falsification in infinite-state systems
• Translating Xd-C programs to MSVL programs
• Verifying a scheduling protocol of safety-critical systems
• scientific article; zbMATH DE number 1755146 (Why is no real title available?)
• Fold/unfold transformations for fixpoint logic
• Temporal verification of programs via first-order fixpoint logic
• Choose your proofs: commutativity and symmetry for smarter reasoning
• Symbolic execution for refuting hyperproperties
• Automatic detection of vulnerable variables for CTL properties of programs

Describes a project that uses

Uses Software

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

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)