A BDD-based model checker for recursive programs
From MaRDI portal
Recommendations
- SMT-based model checking for recursive programs
- Using models to model-check recursive schemes
- Using models to model-check recursive schemes
- Model Checking Recursive Programs with Exact Predicate Abstraction
- LTL model checking for recursive programs
- Resource-constrained model checking of recursive programs
- Model-checking higher-order programs with recursive types
- Model checking and higher-order recursion
- Bounded model checking of recursive programs with pointers in K
Cited in
(32)- Automatic verification of recursive procedures with one integer parameter.
- Pushdown timed automata: A binary reachability characterization and safety verification.
- Analyzing pushdown systems with stack manipulation
- Model checking LTL with regular valuations for pushdown systems
- Verifying parallel programs with dynamic communication structures
- Faster pushdown reachability analysis with applications in network verification
- Multi-matching nested relations
- A generic framework for checking semantic equivalences between pushdown automata and finite-state automata
- Verification of Boolean programs with unbounded thread creation
- Bebop: A symbolic model checker for Boolean programs
- Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection
- Bounded model checking of recursive programs with pointers in K
- Efficient CTL model-checking for pushdown systems
- Model checking procedural programs
- Model checking concurrent programs
- Complete SAT-Based Model Checking for Context-Free Processes
- Model Checking Recursive Programs with Exact Predicate Abstraction
- An automata-theoretic approach to infinite-state systems
- Verifying Parallel Programs with Dynamic Communication Structures
- LTL model checking for recursive programs
- Efficient CTL model-checking for pushdown systems
- A model checking-based approach for security policy verification of mobile systems
- Resource-constrained model checking of recursive programs
- Automatic verification of recursive procedures with one integer parameter
- SMT-based model checking for recursive programs
- View abstraction -- a tutorial (invited paper)
- A Branching Time Variant of CaRet
- Regular model checking: evolution and perspectives
- Verification of programs with exceptions through operator precedence automata
- Pushdown Systems
- Summarization for termination: No return!
- On the complexity of checking semantic equivalences between pushdown processes and finite-state processes
This page was built for publication: A BDD-based model checker for recursive programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4551162)
