Combining static and dynamic approaches to software verification

Initially considered as orthogonal research fields, static and dynamic analysis techniques have been for a long time used separately to improve the quality of software. However, the development of both approaches has led to the discovery of common issues and to the realization of potential synergies. The present talk gives an overview of some of the combinations between static and dynamic verification approaches that were realized in the context of Frama-C, a framework for static and dynamic analysis of C programs developed at CEA LIST.

First, we illustrate how static analysis can be used to help test generation. The SANTE tool takes advantage of abstract interpretation and program slicing in order to achieve more precise detection of runtime errors. These ideas have been pushed further in the LTest tool in order to optimize automatic test generation for a large class of coverage criteria, through the detection of infeasible test objectives.

Second, we illustrate how test generation can in turn help static analysis. We explore in the StaDy tool how program proof and test generation can be combined in order to help the validation engineer to understand and to fix proof failures during deductive verification of programs.

Finally, we show how runtime verification can take benefit of static analysis in order to avoid the monitoring of irrelevant variables and statements (E-ACSL tool).

Sébastien Bardin obtained his PhD in 2005 at ENS Cachan, France, under the guidance of Pr. Alain Finkel. His doctoral work was centered on the verification of infinite-state systems by means of model checking, symbolic representations and loop acceleration. He also co-developed the infinite-state model-checker FAST. After one year as a teaching associate at ENS Cachan, he joined CEA LIST, France, in 2006 as a full-time researcher. His current main research interests are the automatic analysis of executable files, white-box test generation through dynamic symbolic execution and constraint solving. He is one of the main developer of the binary-level test data generation tool OSMOSE, and the Principal Investigator of the ANR BINSEC project (2013-2017) about binary-level security analyses.

Nikolai Kosmatov works as a researcher at the Software Safety Lab of CEA LIST, one of the biggest research centers in France. Nikolai obtained M.Sc. degree in Mathematics at Saint-Petersburg State University in 1997, and Ph.D. in Mathematics jointly at Saint-Petersburg State University and the University of Besançon in 2001. After receiving M.Sc. degree in Computer Science at the University of Besançon in 2003, Nikolai’s research interests have focused on software testing, constraint solving and combinations of various software verification techniques. He is the main author of the online testing service pathcrawler-online.com. He co-organized tutorials on software testing, deductive verification and runtime assertion checking at several international events (TAP 2012, TAROT 2012, ASE 2012, QSIC 2012, TAP 2013, iFM 2013, SAC 2013, RV 2013, TAP 2014), and teaches software verification in several French universities.