Refine my results

Craig Interpolation and proof manipulation : Theory and applications to model checking

Rollini, Simone Fulvio ; Sharygina, Natasha (Dir.)

Thèse de doctorat : Università della Svizzera italiana, 2013 ; 2013INFO006.

Model checking is one of the most appreciated methods for automated formal verification of software and hardware systems. The main challenge in model checking, i.e. scalability to complex systems of extremely large size, has been successfully addressed by means of symbolic techniques, which rely on an efficient representation and manipulation of the systems based on first order logic....