Sharygina, Natasha Fedyukovich, Grigory 2015-12-10 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 guessing a relation and checking whether it is a simulation relation. We present a novel algorithm for discovering simulations symbolically, by means of solving ∀∃-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. application/pdf https://n2t.net/ark:/12658/srd1318701 https://susi.usi.ch/global/documents/318701 https://susi.usi.ch/documents/318701/files/2015INFO013.pdf eng info:eu-repo/semantics/altIdentifier/urn/urn:nbn:ch:rero-006-114964 info:eu-repo/semantics/altIdentifier/ark/12658/srd1318701 info:eu-repo/semantics/openAccess License undefined Software analysis Incremental analysis Formal verification Model checking Bounded model checking Unbounded model checking Invariant inference Symbolic reasoning Abstraction Simulation relation Inductive synthesis SAT solving SMT solving Craig interpolation Quantifier elimination Skolemization Horn clauses info:eu-repo/classification/udc/004 Automated incremental software verification http://purl.org/coar/resource_type/c_db06