The Burden of High-Level Languages: Complicated Symbolic Model Checking

Abstract

Symbolic model checking algorithms like IC3 have proven to be an effective technique for hardware model checking. Extensions to software model checking have been suggested and implemented and seem promising so far. However, using symbolic model checking algorithms for the specification languages B and Event-B is complicated. This is due to their high-level nature, which accounts for complex constraints. While some problems can be coped with by modifications to the algorithms, others relate to the heart of our tools: the constraint solver.