Space-Efficient Bounded Model Checking

Jacob Katz, Ziyad Hanna, Nachum Dershowitz

Current algorithms for bounded model checking use SAT methods for checking satisfiability of Boolean formulae. These methods suffer from the potential memory explosion problem. Met…