Grigory Fedyukovich successfully defended his PhD thesis "Automated Software Incremental Verification".

Abstract:

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 abstraction. However, the majority of the state-of-the-art model checkers are designed that each new software version has to be verified from scratch.

In this dissertation, we investigate the new Formal Incremental Verification (FIV) techniques that aim at making software analysis more efficient by reusing invested efforts between verification runs. In order to show that FIV can be built on the top of different verification techniques, we focus on three complementary approaches to automated formal verification.

First, we contribute the FIV-technique for SAT-based Bounded Model Checking developed to verify programs with (possibly recursive) functions with respect to the set of pre-defined assertions. We present the function-summarization framework based on Craig interpolation that allows extracting and reusing over-approximations of the function behaviors. We introduce the algorithm to revalidate the summaries of one program locally in order to prevent re-verification of another program from scratch.

Second, we contribute the technique for simulation relation synthesis for loop-free programs that do not necessarily contain assertions. We introduce an SMT-based abstraction-refinement algorithm that proceeds by iterative guessing a relation and checking whether it is a simulation relation. We present a novel algorithm for discovering simulations symbolically, by means of solving forall-exists-formulas and extracting witnessing Skolem relations.

Third, we contribute the FIV-technique for SMT-based Unbounded Model Checking developed to verify programs with (possibly nested) loops. We present an algorithm that automatically derives simulations between programs with different loop structures. The automatically synthesized simulation relation is then used to migrate the safe inductive invariants across the evolution boundaries. 

Finally, we contribute the implementation and evaluation of all our algorithmic contributions, and confirm that the state-of-the-art model checking tools can successfully be extended by the FIV-capabilities.

 

Dissertation Committee:

-          Prof. Natasha Sharygina, Università della Svizzera italiana, Switzerland (Research Advisor)

-          Prof. Walter Binder, Università della Svizzera italiana, Switzerland (Internal Member)

-          Prof. Igor Pivkin, Università della Svizzera italiana, Switzerland (Internal Member)

-          Prof. Rupak Majumbar, Max Planck Institute for Software Systems, Germany (External Member)

-          Prof. Thomas Wahl, Northeastern University, USA (External Member)