Automatic discovery of fair paths in infinite-state transition systems

DOI10.1007/978-3-030-88885-5_3zbMath1497.68290OpenAlexW3207031131MaRDI QIDQ2147176

Alberto Griggio, Alessandro Cimatti, Enrico Magnago

Publication date: 22 June 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-88885-5_3

zbMATH Keywords

infinite-state systemsSMTLTL falsificationLTL model checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

Verification Modulo theories ⋮ \textsc{LTL} falsification in infinite-state systems

Uses Software

• Yices
• Uppaal
• z3
• SMTInterpol
• Ultimate Automizer
• AProVE
• MathSAT5
• PySMT

Cites Work

• Unnamed Item
• A compositional approach to CTL\(^*\) verification
• Proving the existence of fair paths in infinite-state systems
• Geometric nontermination arguments
• Temporal property verification as a program analysis task
• Model checking with strong fairness
• Proving non-termination
• Proving Termination of Programs Automatically with AProVE
• Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
• Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems
• SMT-Based Induction Methods for Timed Systems
• Ranking Templates for Linear Loops
• The MathSAT5 SMT Solver
• Formal Methods for the Design of Real-Time Systems
• Two Consequences of the Transposition Theorem on Linear Inequalities
• Termination of triangular Integer loops is decidable