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


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.

Presented at PhD Symposium at 12th International Conference on integrated Formal Methods (iFM 2016)
Sebastian Krings
Sebastian Krings
Software Engineer

My interests include software analysis, formal methods and offensive security.