Bounded model checking of infinite state systems
From MaRDI portal
Publication:2369883
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
Cites work
- A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
- A lattice-theoretical fixpoint theorem and its applications
- A unified framework for race analysis of asynchronous networks
- An axiomatic proof technique for parallel programs
- BerkMin: A fast and robust SAT-solver
- Bounded model checking using satisfiability solving
- Cache behavior prediction by abstract interpretation
- Computer Aided Verification
- Decision problems forω-automata
- Efficient manipulation of decision diagrams
- Graph-Based Algorithms for Boolean Function Manipulation
- GRASP: a search algorithm for propositional satisfiability
- scientific article; zbMATH DE number 52748 (Why is no real title available?)
- scientific article; zbMATH DE number 108539 (Why is no real title available?)
- scientific article; zbMATH DE number 3467028 (Why is no real title available?)
- scientific article; zbMATH DE number 1059247 (Why is no real title available?)
- scientific article; zbMATH DE number 1142314 (Why is no real title available?)
- scientific article; zbMATH DE number 1150567 (Why is no real title available?)
- scientific article; zbMATH DE number 1956571 (Why is no real title available?)
- scientific article; zbMATH DE number 1979550 (Why is no real title available?)
- scientific article; zbMATH DE number 2040893 (Why is no real title available?)
- scientific article; zbMATH DE number 1927430 (Why is no real title available?)
- scientific article; zbMATH DE number 1479635 (Why is no real title available?)
- scientific article; zbMATH DE number 1538036 (Why is no real title available?)
- scientific article; zbMATH DE number 1555955 (Why is no real title available?)
- scientific article; zbMATH DE number 1786477 (Why is no real title available?)
- scientific article; zbMATH DE number 2087217 (Why is no real title available?)
- scientific article; zbMATH DE number 2090318 (Why is no real title available?)
- scientific article; zbMATH DE number 2090515 (Why is no real title available?)
- scientific article; zbMATH DE number 3368555 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- Improving automata generation for linear temporal logic by considering the automaton hierarchy
- Introduction to algorithms
- Local model checking for infinite state spaces
- Local model checking in the modal mu-calculus
- On languages with two variables
- On Preservation Theorems for Two-Variable Logic
- On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
- On the Decision Problem for Two-Variable First-Order Logic
- On ω-regular sets
- Symbolic model checking: \(10^{20}\) states and beyond
- Tableau-based model checking in the propositional mu-calculus
- Temporal logic can be more expressive
- Verification on infinite structures.
- Verification, Model Checking, and Abstract Interpretation
Cited in
(29)- Fixed point characterization of infinite behavior of finite-state systems
- Reducing bounded realizability analysis to reachability checking
- A bounded model checker for three-valued abstractions of concurrent software systems
- Bounded model checking of traffic light control system
- scientific article; zbMATH DE number 1615252 (Why is no real title available?)
- BMC via on-the-fly determinization
- Bounded model checking for all regular properties
- Computing over-approximations with bounded model checking
- EPR-based bounded model checking at word level
- On bounded specifications
- Model checking using description logic
- Formal Verification of Infinite-State BIP Models
- A New Approach to Bounded Model Checking for Branching Time Logics
- Formal Verification of Infinite State Systems Using Boolean Methods
- Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
- Bounded model checking of ETL cooperating with finite and looping automata connectives
- Constraint LTL satisfiability checking without automata
- scientific article; zbMATH DE number 2090318 (Why is no real title available?)
- Bounded model checking of C programs using event automaton specifications
- Algebraic Methodology and Software Technology
- Bounded Model Checking with Description Logic Reasoning
- Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time
- Bounded Model Checking for Partial Kripke Structures
- Verification, Model Checking, and Abstract Interpretation
- Bounded Model Checking for Weak Alternating Büchi Automata
- Convergence testing in term-level bounded model checking
- Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
- Latticed \(k\)-induction with an application to probabilistic programs
- Action language verifier: An infinite-state model checker for reactive software specifications
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)
