Bounded model checking of infinite state systems
From MaRDI portal
Publication:2369883
DOI10.1007/s10703-006-0019-9zbMath1117.68047OpenAlexW2003378122MaRDI QIDQ2369883
Klaus Schneider, Tobias Schuele
Publication date: 21 June 2007
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-006-0019-9
Bounded model checkingInfinite state systemsGlobal model checkingLocal model checkingTemporal logic hierarchy
Related Items
Latticed \(k\)-induction with an application to probabilistic programs, Action language verifier: An infinite-state model checker for reactive software specifications, Constraint LTL satisfiability checking without automata
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Tableau-based model checking in the propositional mu-calculus
- Local model checking in the modal mu-calculus
- Local model checking for infinite state spaces
- Symbolic model checking: \(10^{20}\) states and beyond
- An axiomatic proof technique for parallel programs
- A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
- Efficient manipulation of decision diagrams
- Cache behavior prediction by abstract interpretation
- BerkMin: A fast and robust SAT-solver
- A lattice-theoretical fixpoint theorem and its applications
- Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy
- Temporal logic can be more expressive
- On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
- Graph-Based Algorithms for Boolean Function Manipulation
- A unified framework for race analysis of asynchronous networks
- On ω-regular sets
- On languages with two variables
- On Preservation Theorems for Two-Variable Logic
- On the Decision Problem for Two-Variable First-Order Logic
- GRASP: a search algorithm for propositional satisfiability
- Computer Aided Verification
- Decision problems forω-automata
- Verification, Model Checking, and Abstract Interpretation
- Bounded model checking using satisfiability solving
