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