Affiner les résultats

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