Bebop

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 70 articles )

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

1 2 3 4 next

  1. Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh: Hybrid automata-based CEGAR for rectangular hybrid systems (2015)
  2. Bozzelli, Laura; Sánchez, César: Visibly rational expressions (2014)
  3. Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh: Hybrid automata-based CEGAR for rectangular hybrid systems (2013)
  4. Braghin, Chiara; Sharygina, Natasha; Barone-Adesi, Katerina: A model checking-based approach for security policy verification of mobile systems (2011)
  5. Braman, Julia M.B.; Murray, Richard M.: Bisimulation conversion and verification procedure for goal-based control systems (2011)
  6. Hague, Matthew: Parameterised pushdown systems with non-atomic writes (2011)
  7. Hague, M.; Ong, C.-H.L.: A saturation method for the modal $\mu $-calculus over pushdown systems (2011)
  8. Schlich, Bastian; Brauer, Jörg; Kowalewski, Stefan: Application of static analyses for state-space reduction to the microcontroller binary code (2011)
  9. Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; Kroening, Daniel: Context-aware counter abstraction (2010)
  10. Collavizza, Hélène; Rueher, Michel; Van Hentenryck, Pascal: CPBPV: a constraint-programming framework for bounded program verification (2010)
  11. Godefroid, Patrice; Nori, Aditya V.; Rajamani, Sriram K.; Tetali, Sai Deep: Compositional may-must program analysis: unleashing the power of alternation (2010)
  12. Kroening, Daniel; Weissenbacher, Georg: Verification and falsification of programs with loops using predicate abstraction (2010)
  13. Cook, Byron; Podelski, Andreas; Rybalchenko, Andrey: Summarization for termination: No return! (2009)
  14. Etessami, Kousha; Godefroid, Patrice: An abort-aware model of transactional programming (2009)
  15. Hague, Matthew; Ong, C.-H.Luke: Winning regions of pushdown parity games: a saturation method (2009)
  16. Lal, Akash; Reps, Thomas: Reducing concurrent analysis under a context bound to sequential analysis (2009)
  17. Schlich, Bastian; Kowalewski, Stefan: Model checking C source code for embedded systems (2009)
  18. Alur, Rajeev; Arenas, Marcelo; Barcelo, Pablo; Etessami, Kousha; Immerman, Neil; Libkin, Leonid: First-order and temporal logics for nested words (2008)
  19. Bakewell, Adam; Ghica, Dan R.: On-the-fly techniques for game-based software model checking (2008)
  20. Ivančić, Franjo; Yang, Zijiang; Ganai, Malay K.; Gupta, Aarti; Ashar, Pranav: Efficient SAT-based bounded model checking for software verification (2008)

1 2 3 4 next