Bounded model checking of infinite state systems
From MaRDI portal
Publication:2369883
DOI10.1007/S10703-006-0019-9zbMATH Open1117.68047OpenAlexW2003378122MaRDI QIDQ2369883FDOQ2369883
Authors: Tobias Schuele, Klaus Schneider 
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
Recommendations
- scientific article; zbMATH DE number 1799521
- Accelerating bounded model checking of safety properties
- A New Approach to Bounded Model Checking for Branching Time Logics
- Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
- Bounded model checking for the existential fragment of \(\mathrm{TCTL}_{-G}\) and diagonal timed automata
Bounded model checkingInfinite state systemsGlobal model checkingLocal model checkingTemporal logic hierarchy
Cites Work
- BerkMin: A fast and robust SAT-solver
- Title not available (Why is that?)
- Introduction to algorithms
- Graph-Based Algorithms for Boolean Function Manipulation
- Cache behavior prediction by abstract interpretation
- Title not available (Why is that?)
- Title not available (Why is that?)
- Symbolic model checking: \(10^{20}\) states and beyond
- A lattice-theoretical fixpoint theorem and its applications
- Verification, Model Checking, and Abstract Interpretation
- Temporal logic can be more expressive
- Title not available (Why is that?)
- Verification on infinite structures.
- Title not available (Why is that?)
- Title not available (Why is that?)
- GRASP: a search algorithm for propositional satisfiability
- A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
- On the Decision Problem for Two-Variable First-Order Logic
- An axiomatic proof technique for parallel programs
- On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
- On languages with two variables
- Title not available (Why is that?)
- Bounded model checking using satisfiability solving
- Title not available (Why is that?)
- Efficient manipulation of decision diagrams
- Title not available (Why is that?)
- Title not available (Why is that?)
- Decision problems forω-automata
- Tableau-based model checking in the propositional mu-calculus
- Local model checking in the modal mu-calculus
- On ω-regular sets
- Title not available (Why is that?)
- Title not available (Why is that?)
- Local model checking for infinite state spaces
- Title not available (Why is that?)
- Title not available (Why is that?)
- Computer Aided Verification
- A unified framework for race analysis of asynchronous networks
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Improving automata generation for linear temporal logic by considering the automaton hierarchy
- On Preservation Theorems for Two-Variable Logic
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (29)
- Title not available (Why is that?)
- Latticed \(k\)-induction with an application to probabilistic programs
- Constraint LTL satisfiability checking without automata
- Formal Verification of Infinite-State BIP Models
- Bounded Model Checking with Description Logic Reasoning
- Action language verifier: An infinite-state model checker for reactive software specifications
- Algebraic Methodology and Software Technology
- Bounded Model Checking for Weak Alternating Büchi Automata
- Bounded model checking for all regular properties
- A New Approach to Bounded Model Checking for Branching Time Logics
- Fixed point characterization of infinite behavior of finite-state systems
- Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
- Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
- Reducing bounded realizability analysis to reachability checking
- Model checking using description logic
- A bounded model checker for three-valued abstractions of concurrent software systems
- Convergence testing in term-level bounded model checking
- EPR-based bounded model checking at word level
- Bounded model checking of ETL cooperating with finite and looping automata connectives
- Bounded model checking of C programs using event automaton specifications
- Verification, Model Checking, and Abstract Interpretation
- On bounded specifications
- Bounded Model Checking for Partial Kripke Structures
- Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time
- Computing over-approximations with bounded model checking
- BMC via on-the-fly determinization
- Formal Verification of Infinite State Systems Using Boolean Methods
- Title not available (Why is that?)
- Bounded model checking of traffic light control system
Uses Software
This page was built for publication: Bounded model checking of infinite state systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2369883)
