Interpolants and Symbolic Model Checking
From MaRDI portal
Publication:5452599
DOI10.1007/978-3-540-69738-1_6zbMATH Open1132.68474OpenAlexW1564176330MaRDI QIDQ5452599FDOQ5452599
Authors: K. L. McMillan 
Publication date: 4 April 2008
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-69738-1_6
Recommendations
Cited In (55)
- Computation tree logic model checking based on multi-valued possibility measures
- Computer Science Logic
- Reasoning about nondeterministic and concurrent actions: A process algebra approach
- Nested interpolants
- Model checking of linear-time properties in multi-valued systems
- The state of SAT
- On the universal and existential fragments of the \(\mu\)-calculus
- State-set branching: leveraging BDDs for heuristic search
- Finding Guaranteed MUSes Fast
- Programming Combinations of Deduction and BDD-based Symbolic Calculation
- Effectively propositional interpolants
- Linear reachability problems and minimal solutions to linear Diophantine equation systems
- Strong planning under partial observability
- Conformant planning via symbolic model checking and heuristic search
- Test generation from P systems using model checking
- Star-topology decoupled state space search
- Module checking
- BDD-based symbolic model checking
- Compositional SCC analysis for language emptiness
- Interpolant strength
- Symbolic model checking with rich assertional languages
- Applications and Theory of Petri Nets 2005
- Correct Hardware Design and Verification Methods
- An efficient algorithm for the parallel solution of high-dimensional differential equations
- A framework for the verification of infinite-state graph transformation systems
- Integrating external deduction tools with ACL2
- A local approach for temporal model checking of Java bytecode
- Probabilistic temporal logics via the modal mu-calculus
- Formal verification of concurrent systems via directed model checking
- Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic
- Efficient generation of small interpolants in CNF
- On the order of test goals in specification-based testing
- New developments in the theory of Gröbner bases and applications to formal verification
- Probably approximately correct interpolants generation
- Efficient symbolic search for cost-optimal planning
- Contextual Petri nets, asymmetric event structures, and processes
- Domain and event structure semantics for Petri nets with read and inhibitor arcs
- Specification in CTL + past for verification in CTL.
- Title not available (Why is that?)
- An automatic abstraction technique for verifying featured, parameterised systems
- An interpolating theorem prover
- Polybori: A framework for Gröbner-basis computations with Boolean polynomials
- Wu's characteristic set method for SystemVerilog assertions verification
- An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
- Interpolation Properties and SAT-Based Model Checking
- Ground interpolation for the theory of equality
- Action and knowledge in alternating-time temporal logic
- AND/OR search spaces for graphical models
- Tools and Algorithms for the Construction and Analysis of Systems
- Formal reliability analysis of redundancy architectures
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- Interpolant learning and reuse in SAT-based model checking
- Ground Interpolation for the Theory of Equality
- Dynamic Path Reduction for Software Model Checking
- Computation tree logic model checking based on possibility measures
This page was built for publication: Interpolants and Symbolic Model Checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5452599)
