Università della Svizzera italiana

Automated incremental software verification

Fedyukovich, Grigory ; Sharygina, Natasha (Dir.)

Thèse de doctorat : Università della Svizzera italiana, 2015 ; 2015INFO013.

Software continuously evolves to meet rapidly changing human needs. Each evolved transformation of a program is expected to preserve important correctness and security properties. Aiming to assure program correctness after a change, formal verification techniques, such as Software Model Checking, have recently benefited from fully automated solutions based on symbolic reasoning and...

Università della Svizzera italiana

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....