Symbolic model checking: 10²⁰ states and beyond
From MaRDI portal
Publication:1193587
Recommendations
- Model-Checking Large Finite-State Systems and Beyond
- Symbolic Model Checking of Infinite-State Systems Using Narrowing
- Symbolic model checking in non-Boolean domains
- scientific article; zbMATH DE number 1670519
- scientific article; zbMATH DE number 1487478
- Model Checking – My 27-Year Quest to Overcome the State Explosion Problem
- Symbolic model checking with rich assertional languages
Cites work
- A calculus of communicating systems
- A partial approach to model checking
- A unified approach for showing language inclusion and equivalence between various types of -automata
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Automatic Verification of Sequential Circuits Using Temporal Logic
- Calculi for synchrony and asynchrony
- Graph-Based Algorithms for Boolean Function Manipulation
- scientific article; zbMATH DE number 3767031 (Why is no real title available?)
- scientific article; zbMATH DE number 50588 (Why is no real title available?)
- scientific article; zbMATH DE number 67477 (Why is no real title available?)
- scientific article; zbMATH DE number 177513 (Why is no real title available?)
- Local model checking in the modal mu-calculus
- On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
- Results on the propositional \(\mu\)-calculus
- Symbolic model checking: \(10^{20}\) states and beyond
Cited in
(only showing first 100 items - show all)- Representation of graphs by OBDDs
- Partitioned PLTL model-checking for refined transition systems
- Hybrid systems: From verification to falsification by combining motion planning and discrete search
- Model checking for hybrid logic
- Symbolic model checking: \(10^{20}\) states and beyond
- A theory of timed automata
- Model checking for action-based logics
- An exercise in the automatic verification of asynchronous designs
- Efficient data structures for Boolean functions
- Fast and simple nested fixpoints
- Petri nets, traces, and local model checking
- An improved algorithm for the evaluation of fixpoint expressions
- Program schemata vs. automata for decidability of program logics
- On the expressivity and complexity of quantitative branching-time temporal logics
- Well-abstracted transition systems: Application to FIFO automata.
- A satisfiability procedure for quantified Boolean formulae
- Binary decision diagrams for first-order predicate logic.
- Symbolic state-space exploration and numerical analysis of state-sharing composed models
- Symbolic model checking for -calculus requires exponential time
- Stochastic dynamic programming with factored representations
- Generating model checkers from algebraic specifications
- Randomized OBDD-based graph algorithms
- Practical verification of multi-agent systems against \textsc{Slk} specifications
- Symbolic perimeter abstraction heuristics for cost-optimal planning
- An explicit transition system construction approach to LTL satisfiability checking
- Symbolic checking of fuzzy CTL on fuzzy program graph
- Model checking properties on reduced trace systems
- Hybrid and subexponential linear logics
- The complexity of counting models of linear-time temporal logic
- Structuring and automating hardware proofs in a higher-order theorem- proving environment
- Decidable integration graphs.
- Specification in CTL + past for verification in CTL.
- NuSMV: A new symbolic model checker
- Iterating transducers
- Syntax-directed model checking of sequential programs
- From pre-historic to post-modern symbolic model checking
- The temporal boolean derivative applied to verification of extended finite state machines
- Symbolic synthesis of masking fault-tolerant distributed programs
- Exponential improvement of time complexity of model checking for multiagent systems with perfect recall
- Formal verification based on Boolean expression diagrams
- Discrete-time control for rectangular hybrid automata
- Compositional reasoning for shared-variable concurrent programs
- On the number of active states in finite automata
- Generating extended resolution proofs with a BDD-based SAT solver
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
- Pardinus: a temporal relational model finder
- Lazy regular sensing
- Improving the filtering of branch-and-bound MDD solver
- Automata-driven partial order reduction and guided search for LTL model checking
- Symbolic model checking with sentential decision diagrams
- First-order temporal logic monitoring with BDDs
- Static analysis and stochastic search for reachability problem
- Symbolic coloured SCC decomposition
- Verification and enforcement of access control policies
- Approximate verification of strategic abilities under imperfect information
- Two AGM-style characterizations of model repair
- An automata-theoretic approach to model-checking systems and specifications over infinite data domains
- Counterexample-preserving reduction for symbolic model checking
- Terminal satisfiability in GSTE
- The complexity of automated addition of fault-tolerance without explicit legitimate states
- On the universal and existential fragments of the \(\mu\)-calculus
- Bounded model checking of infinite state systems
- Verification of SpecC using predicate abstraction
- Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams
- Symbolic model checking for probabilistic timed automata
- GSTE is partitioned model checking
- On the number of active states in deterministic and nondeterministic finite automata
- Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes
- Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
- Temporal property verification as a program analysis task
- Priority functions for the approximation of the metric TSP
- Properties of a predicate transformer of the VRS system
- An automatic method for the dynamic construction of abstractions of states of a formal model
- Strong planning under partial observability
- Concurrent reachability games
- Symbolic topological sorting with OBDDs
- Symbolic graphs: Linear solutions to connectivity related problems
- ACTLW -- an action-based computation tree logic with unless operator
- Abstractions of data types
- Model checking with strong fairness
- Qualitative criteria of admissibility for enforced agreements
- A contribution to the validation of grafcet controlled systems
- Bounded model checking of traffic light control system
- From complementation to certification
- An interpolating theorem prover
- Exploiting interleaving semantics in symbolic state-space generation
- Program verification with interacting analysis plugins
- When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus
- The state of SAT
- Extracting unsatisfiable cores for LTL via temporal resolution
- A proof system for unified temporal logic
- scientific article; zbMATH DE number 1630131 (Why is no real title available?)
- On the unusual effectiveness of logic in computer science
- Towards an efficient library for SAT: A manifesto
- scientific article; zbMATH DE number 1670517 (Why is no real title available?)
- scientific article; zbMATH DE number 1696437 (Why is no real title available?)
- scientific article; zbMATH DE number 1701750 (Why is no real title available?)
- scientific article; zbMATH DE number 1701767 (Why is no real title available?)
- Compositional model checking of product-form CTMCs
- Formal models of timing attacks on web privacy
This page was built for publication: Symbolic model checking: \(10^{20}\) states and beyond
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1193587)
