Affiner les résultats

Controlled and effective interpolation

de Sá Alt, Leonardo ; Sharygina, Natasha (Dir.)

Thèse de doctorat : Università della Svizzera italiana, 2016 ; 2016INFO009.

Model checking is a well established technique to verify systems, exhaustively and automatically. The state space explosion, known as the main difficulty in model checking scalability, has been successfully approached by symbolic model checking which represents programs using logic, usually at the propositional or first order theories level. Craig interpolation is one of the most successful...