Contract Based Program Models for Software Model Checking

Jesper Amilon, Dilian Gurov

Model checking temporal properties of software is algorithmically hard. To be practically feasible, it usually requires the creation of simpler, abstract models of the software, ov…