Bebop: A symbolic model checker for Boolean programs
From MaRDI portal
Recommendations
Cited in
(55)- Types and trace effects for object orientation
- Reducing concurrent analysis under a context bound to sequential analysis
- Pushdown timed automata: A binary reachability characterization and safety verification.
- Analyzing pushdown systems with stack manipulation
- Syntax-directed model checking of sequential programs
- Model checking LTL with regular valuations for pushdown systems
- A formal model for detecting bugs by symbolic execution of programs
- Modular strategies for recursive game graphs
- Counterexample-guided predicate abstraction of hybrid systems
- Visibly rational expressions
- The word problem for visibly pushdown languages described by grammars
- Verification of Boolean programs with unbounded thread creation
- Program verification with interacting analysis plugins
- Faster algorithms for weighted recursive state machines
- SAT-Based Model Checking
- Abstraction and abstraction refinement
- Interpolation and model checking
- Predicate abstraction for program verification
- Model checking procedural programs
- Winning Regions of Pushdown Parity Games: A Saturation Method
- Complete SAT-Based Model Checking for Context-Free Processes
- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
- Splitting the Control Flow with Boolean Flags
- Rewriting Models of Boolean Programs
- Model Checking Recursive Programs with Exact Predicate Abstraction
- An Infinite Automaton Characterization of Double Exponential Time
- An automata-theoretic approach to infinite-state systems
- Reducing behavioural to structural properties of programs with procedures
- A model checking-based approach for security policy verification of mobile systems
- scientific article; zbMATH DE number 1982200 (Why is no real title available?)
- A first-order complete temporal logic for structured context-free languages
- VLDL satisfiability and model checking via tree automata
- SMT-based model checking for recursive programs
- Ramsey-based inclusion checking for visibly pushdown automata
- Computer Aided Verification
- A saturation method for the modal \(\mu \)-calculus over pushdown systems
- On-the-Fly Techniques for Game-Based Software Model Checking
- Program Analysis Using Weighted Pushdown Systems
- Minimization, Learning, and Conformance Testing of Boolean Programs
- Context-aware counter abstraction
- Verification of programs with exceptions through operator precedence automata
- Application of static analyses for state-space reduction to the microcontroller binary code
- Bisimulation conversion and verification procedure for goal-based control systems
- Visibly linear temporal logic
- Module checking of pushdown multi-agent systems
- Verifying time partitioning in the DEOS scheduling kernel
- Translating Java for multiple model checkers: The Bandera back-end
- Model-checking structured context-free languages
- Summarization for termination: No return!
- An abstract interpretation toolkit for CRL
- Hybrid automata-based CEGAR for rectangular hybrid systems
- Efficient SAT-based bounded model checking for software verification
- Verification of scope-dependent hierarchical state machines
- Verification and falsification of programs with loops using predicate abstraction
- CPBPV: a constraint-programming framework for bounded program verification
This page was built for publication: Bebop: A symbolic model checker for Boolean programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2753756)
