\textsc{LTL} falsification in infinite-state systems
From MaRDI portal
Publication:2105460
DOI10.1016/J.IC.2022.104977OpenAlexW4307210883MaRDI QIDQ2105460FDOQ2105460
Authors: 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
Recommendations
- Automatic discovery of fair paths in infinite-state transition systems
- Proving the existence of fair paths in infinite-state systems
- Infinite-state liveness-to-safety via implicit abstraction and well-founded relations
- Falsification of LTL Safety Properties in Hybrid Systems
- Fairness modulo theory: a new approach to LTL software model checking
first-order linear-time temporal logicinfinite-state transition systemsSMT-based model checkingtemporal satisfiability
Cites Work
- Formal Methods for the Design of Real-Time Systems
- The MathSAT5 SMT solver
- A theory of timed automata
- The benefits of relaxing punctuality
- Geometric nontermination arguments
- 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 compositional approach to CTL\(^*\) verification
- On the decidability of continuous time specification formalisms
- 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
- Temporal property verification as a program analysis task
- Proving non-termination
- Infinite-state liveness-to-safety via implicit abstraction and well-founded relations
- Computer Aided Verification
- Two Consequences of the Transposition Theorem on Linear Inequalities
- A new look at the automatic synthesis of linear ranking functions
- Ranking Templates for Linear Loops
- A constraint-based approach to solving games on infinite graphs
- Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems
- Model checking with strong fairness
- GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
- Compositional reasoning
- 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
- Proving the existence of fair paths in infinite-state systems
- Proving termination of programs automatically with AProVE
- Automatic discovery of fair paths in infinite-state transition systems
- Region Stability Proofs for Hybrid Systems
- Verifying increasingly expressive temporal logics for infinite-state systems
Cited In (1)
Uses Software
This page was built for publication: \textsc{LTL} falsification in infinite-state systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2105460)
