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

An SMT-based verification framework for software systems handling arrays

Alberti, Francesco ; Sharygina, Natasha (Dir.)

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

Università della Svizzera italiana

Scalable abstractions for efficient security checks

Tsitovich, Aliaksei ; Sharygina, Natasha (Dir.)

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