Liveness checking as safety checking for infinite state spaces

zbMATH Open1273.68240MaRDI QIDQ2852018FDOQ2852018

Armin Biere, Viktor Schuppan

Publication date: 7 October 2013

Full work available at URL: http://www.sciencedirect.com/science/article/pii/S1571066106000557

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (9)

• Liveness by Invisible Invariants
• Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems
• Survey on Directed Model Checking
• From liveness to promptness
• On relative and probabilistic finite counterability
• Title not available (Why is that?)
• Automata-Theoretic Model Checking Revisited
• Linear temporal logic symbolic model checking
• A unifying view on SMT-based software verification

   Recommendations

• Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations 👍 👎
• Title not available (Why is that?) 👍 👎
• Computer Science Logic 👍 👎
• A lattice-theoretic characterization of safety and liveness 👍 👎
• On reachability and safety in infinite-state systems 👍 👎
• Local model checking for infinite state spaces 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Automated Technology for Verification and Analysis 👍 👎

This page was built for publication: Liveness checking as safety checking for infinite state spaces

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