\textsc{LTL} falsification in infinite-state systems
From MaRDI portal
Publication:2105460
DOI10.1016/j.ic.2022.104977OpenAlexW4307210883MaRDI QIDQ2105460
Alessandro Cimatti, Alberto Griggio, Enrico Magnago
Publication date: 8 December 2022
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2022.104977
first-order linear-time temporal logicinfinite-state transition systemsSMT-based model checkingtemporal satisfiability
Related Items
Uses Software
Cites Work
- Formal techniques for distributed systems. Joint 14th IFIP WG 6.1 international conference, FMOODS 2012 and 32nd IFIP WG 6.1 international conference, FORTE 2012, Stockholm, Sweden, June 13--16, 2012. Proceedings
- A new look at the automatic synthesis of linear ranking functions
- A theory of timed automata
- A compositional approach to CTL\(^*\) verification
- Automatic discovery of fair paths in infinite-state transition systems
- Proving the existence of fair paths in infinite-state systems
- Geometric nontermination arguments
- Temporal property verification as a program analysis task
- Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
- Model checking with strong fairness
- Tools and algorithms for the construction and analysis of systems. 25 years of TACAS: TOOLympics, held as part of ETAPS 2019, Prague, Czech Republic, April 6--11, 2019. Proceedings. Part III
- Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems
- Compositional Reasoning
- Proving non-termination
- Proving Termination of Programs Automatically with AProVE
- GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
- Region Stability Proofs for Hybrid Systems
- On the decidability of continuous time specification formalisms
- The benefits of relaxing punctuality
- Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
- Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems
- Ranking Templates for Linear Loops
- The MathSAT5 SMT Solver
- A constraint-based approach to solving games on infinite graphs
- Formal Methods for the Design of Real-Time Systems
- Computer Aided Verification
- Two Consequences of the Transposition Theorem on Linear Inequalities
