Bebop: A Symbolic Model Checker for Boolean Programs. We present the design, implementation and empirical evaluation of Bebop—a symbolic model checker for boolean programs. Bebop represents control flow explicitly, and sets of states implicitly using BDDs. By harnessing the inherent modularity in procedural abstraction and exploiting the locality of variable scoping, Bebop is able to model check boolean programs with several thousand lines of code, hundreds of procedures, and several thousand variables in a few minutes.

References in zbMATH (referenced in 64 articles )

Showing results 1 to 20 of 64.
Sorted by year (citations)

1 2 3 4 next

  1. Abal, Iago; Brabrand, Claus; Wąsowski, Andrzej: Effective bug finding in C programs with shape and effect abstractions (2017)
  2. Chatterjee, Krishnendu; Kragl, Bernhard; Mishra, Samarth; Pavlogiannis, Andreas: Faster algorithms for weighted recursive state machines (2017)
  3. Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar: SMT-based model checking for recursive programs (2016)
  4. Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh: Hybrid automata-based CEGAR for rectangular hybrid systems (2015)
  5. Bozzelli, Laura; Sánchez, César: Visibly rational expressions (2014)
  6. Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh: Hybrid automata-based CEGAR for rectangular hybrid systems (2013)
  7. Braghin, Chiara; Sharygina, Natasha; Barone-Adesi, Katerina: A model checking-based approach for security policy verification of mobile systems (2011)
  8. Braman, Julia M.B.; Murray, Richard M.: Bisimulation conversion and verification procedure for goal-based control systems (2011)
  9. Hague, Matthew: Parameterised pushdown systems with non-atomic writes (2011)
  10. Hague, M.; Ong, C.-H.L.: A saturation method for the modal $\mu $-calculus over pushdown systems (2011)
  11. Schlich, Bastian; Brauer, Jörg; Kowalewski, Stefan: Application of static analyses for state-space reduction to the microcontroller binary code (2011)
  12. Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel: Context-aware counter abstraction (2010)
  13. Collavizza, Hélène; Rueher, Michel; Van Hentenryck, Pascal: CPBPV: a constraint-programming framework for bounded program verification (2010)
  14. Godefroid, Patrice; Nori, Aditya V.; Rajamani, Sriram K.; Tetali, Sai Deep: Compositional may-must program analysis: unleashing the power of alternation (2010)
  15. Kroening, Daniel; Weissenbacher, Georg: Verification and falsification of programs with loops using predicate abstraction (2010)
  16. Cook, Byron; Podelski, Andreas; Rybalchenko, Andrey: Summarization for termination: No return! (2009)
  17. Etessami, Kousha; Godefroid, Patrice: An abort-aware model of transactional programming (2009)
  18. Hague, Matthew; Ong, C.-H.Luke: Winning regions of pushdown parity games: a saturation method (2009)
  19. Lal, Akash; Reps, Thomas: Reducing concurrent analysis under a context bound to sequential analysis (2009)
  20. Schlich, Bastian; Kowalewski, Stefan: Model checking C source code for embedded systems (2009) ioport

1 2 3 4 next