Automated Incremental Software Verification

Speaker:        Dr. Grigory Fedyukovich
                University of Washington

Title:          "Automated Incremental Software Verification"

Date:           Monday, 24 October 2016

Time:           4:00pm - 5:00pm

Venue:          Lecture Theatre F (near lifts 25/26), HKUST

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 so each new software version
has to be verified from scratch.

In this talk, we outline the new Formal Incremental Verification (FIV)
techniques that aims at making software analysis more efficient by reusing
invested efforts between verification runs. In the heart of our approach,
there is SimAbs, a fully automated SMT-based approach to synthesize an
abstraction of one program (called target) that simulates another program
(called source). SimAbs iteratively traverses the search space of
existential abstractions of the target and choses the strongest
abstraction among them that simulates the source.

Deciding whether a given relation is a simulation relation is reduced to
iterative solving validity of a sequence of ∀∃-formulas. We present a
novel algorithm for dealing with such formulas using an incremental SMT
solver. In addition to deciding validity, our algorithm extracts
witnessing Skolem relations which further drive simulation synthesis in
SimAbs. Our evaluation confirms that SimAbs is able to efficiently
discover both, simulations and abstractions, for C programs from the
Software Verification Competition.


*******************
Biography:

Grigory Fedyukovich is a postdoc at PLSE lab of University of Washington,
USA, working with Prof. Rastislav Bodik. He completed the PhD at Formal
Verification Lab of University of Lugano, Switzerland (2015), under
supervision of Prof. NatashaSharygina. He graduated from Saint Petersburg
State University, Russia (2008), and also did two internships at Institute
of Cybernetics, Estonia (2009); and at National University of Singapore
(2010). The main focus of his research is Interpolation-based Incremental
Model Checking, and Inductive Simulation Synthesis for establishing
Program Equivalence.