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
- 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?)
- 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
- GRASP: a search algorithm for propositional satisfiability
- Graph-Based Algorithms for Boolean Function Manipulation
- 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 Preservation Theorems for Two-Variable Logic
- On languages with two variables
- On the Decision Problem for Two-Variable First-Order Logic
- On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
- 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)- Algebraic Methodology and Software Technology
- Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
- BMC via on-the-fly determinization
- Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
- Computing over-approximations with bounded model checking
- Reducing bounded realizability analysis to reachability checking
- scientific article; zbMATH DE number 2090318 (Why is no real title available?)
- Latticed \(k\)-induction with an application to probabilistic programs
- Formal Verification of Infinite-State BIP Models
- EPR-based bounded model checking at word level
- Bounded model checking of traffic light control system
- Model checking using description logic
- Constraint LTL satisfiability checking without automata
- Bounded model checking of ETL cooperating with finite and looping automata connectives
- On bounded specifications
- Convergence testing in term-level bounded model checking
- Bounded Model Checking for Partial Kripke Structures
- Action language verifier: An infinite-state model checker for reactive software specifications
- Formal Verification of Infinite State Systems Using Boolean Methods
- Fixed point characterization of infinite behavior of finite-state systems
- Bounded model checking for all regular properties
- A New Approach to Bounded Model Checking for Branching Time Logics
- A bounded model checker for three-valued abstractions of concurrent software systems
- scientific article; zbMATH DE number 1615252 (Why is no real title available?)
- Bounded Model Checking with Description Logic Reasoning
- Verification, Model Checking, and Abstract Interpretation
- Bounded model checking of C programs using event automaton specifications
- Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time
- Bounded Model Checking for Weak Alternating Büchi Automata
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)
