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...
|
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...
|
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....
|
Thèse de doctorat : Università della Svizzera italiana, 2011 ; 2011INFO008.
Following the industrial demand to address the problem of software correctness, the computer science research community puts a lot of efforts into development of scalable and precise formal methods that are applicable to industrial-size programs. Unfortunately, most of software verification techniques suffer from the effect of combinatorial blowup also known as a "state-space explosion", i.e.,...
|
Thèse de doctorat : Università della Svizzera italiana, 2015 ; 2015INFO003.
Recent advances in the areas of automated reasoning and first-order theorem proving paved the way to the developing of effective tools for the rigorous formal analysis of computer systems. Nowadays many formal verification frameworks are built over highly engineered tools (SMT-solvers) implementing decision procedures for quantifier- free fragments of theories of interest for (dis)proving...
|
