Interpolants and Symbolic Model Checking
From MaRDI portal
Publication:5452599
DOI10.1007/978-3-540-69738-1_6zbMath1132.68474OpenAlexW1564176330MaRDI QIDQ5452599
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
Related Items
Domain and event structure semantics for Petri nets with read and inhibitor arcs, On the universal and existential fragments of the \(\mu\)-calculus, BDD-Based Symbolic Model Checking, The state of SAT, State-set branching: leveraging BDDs for heuristic search, Efficient symbolic search for cost-optimal planning, Programming Combinations of Deduction and BDD-based Symbolic Calculation, Wu's characteristic set method for SystemVerilog assertions verification, Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic, Finding Guaranteed MUSes Fast, An efficient algorithm for the parallel solution of high-dimensional differential equations, Computation tree logic model checking based on multi-valued possibility measures, Strong planning under partial observability, A framework for the verification of infinite-state graph transformation systems, Formal reliability analysis of redundancy architectures, An automatic abstraction technique for verifying featured, parameterised systems, Star-topology decoupled state space search, Computation tree logic model checking based on possibility measures, Linear reachability problems and minimal solutions to linear Diophantine equation systems, Formal Verification of Concurrent Systems via Directed Model Checking, Symbolic model checking with rich assertional languages, On the order of test goals in specification-based testing, A local approach for temporal model checking of Java bytecode, Action and knowledge in alternating-time temporal logic, Test generation from P systems using model checking, An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps, Compositional SCC analysis for language emptiness, Dynamic Path Reduction for Software Model Checking, Model checking of linear-time properties in multi-valued systems, Integrating external deduction tools with ACL2, New developments in the theory of Gröbner bases and applications to formal verification, AND/OR search spaces for graphical models, Reasoning about nondeterministic and concurrent actions: A process algebra approach, Polybori: A framework for Gröbner-basis computations with Boolean polynomials, Probabilistic temporal logics via the modal mu-calculus, SAT-based explicit LTL reasoning and its application to satisfiability checking, Specification in CTL + past for verification in CTL., Module checking, Contextual Petri nets, asymmetric event structures, and processes, Conformant planning via symbolic model checking and heuristic search
