SciLex Program, April 12, 14.30, room F3.07

  • 14.30 : Christoph Haase, ENS Cachan
Title : The Euler-Hierholzer theorem and its application in the verification of concurrent infinite-state systems
Abstract :Given a directed graph and some vertex v, the Eulerian path problem is to decide whether there exists a path starting and ending in v that visits every edge of the graph exactly once. The Euler-Hierholzer theorem provides an easy characterization of such graphs which has turned out to be particularly useful in the verification of concurrent infinite-state systems and also in other areas. In this talk, I will give an overview about some applications this theorem has found in theory and practice. On the one hand, it was one cornerstone that allowed us to resolve a long standing open problem about the complexity of reachability in two-dimensional vector addition systems with states. On the other hand, it has enabled us to design a highly efficient decision procedure for the Petri net coverability problem that makes the computer-aided verification of concurrent programs feasible.
  • 15.00 Jean-Christophe Léchenet (CEA LIST), Nikolai Kosmatov (CEA LIST) (speaker), Pascale Le Gall (CentraleSupélec)
Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices
Abstract: Program slicing can be used to reduce a given initial program to a smaller one (a slice) which preserves the behavior of the initial program with respect to a chosen criterion. Verification and validation (V&V) of software can become easier on slices, but require particular care in presence of errors or non-termination in order to avoid unsound results. Indeed, both cases can in some sense interrupt normal execution of the program preventing the following statements from being executed. Therefore, slicing away (that is, removing) potentially erroneous or non-terminating sub-programs from the slice can have an impact on soundness of program slicing.
To satisfy the traditional soundness property, program slicing would require to consider additional dependencies of each statement on previous loops and error-prone statements. That would lead to inefficient (that is, too large) slices, where we would systematically preserve all potentially erroneous or non-terminating statements executed before the slicing criterion. Such slices would have very limited benefit for our purpose of performing V&V on slices instead of the initial program.
This work proposes a theoretical foundation for conducting V&V activities on a slice instead of the initial program. We consider errors determined by the current program state such as runtime errors (that can either interrupt the program or lead to an undefined behavior). We also consider a realistic setting of programs with potentially non-terminating loops, even if this non-termination is unintended. So we assume neither that all loops terminate, nor that all loops do not terminate, nor that we have a preliminary knowledge of which loops terminate and which loops do not.
We introduce the notion of relaxed slicing that requires a limited number of dependencies and remains efficient even in presence of errors or non-termination. We establish an appropriate soundness property for relaxed slicing. It allows us to give a precise interpretation of verification results (absence or presence of errors) obtained for a slice in terms of the initial program. All results have been formalized and proved in Coq. This talk is based on a recent publication at ETAPS/FASE 2016.
  • 15. 20 Enhancing Symbolic Execution for Coverage-Oriented Testing
Sébastien Bardin (speaker), Nikolai Kosmatov, Mickaël Delahaye, Robin David (all CEA, LIST)
Abstract: Automatic (code-based) test data generation is a major topic in software engineering, and Dynamic Symbolic Execution (DSE) is a very promising approach to this problem. However, while DSE inherently covers feasible paths of the program under test, practical testing is more concerned with fulfilling so called coverage criteria, such as instruction coverage, branch coverage, MCDC (in aeronautic) or mutations. Three problems arise for DSE in this context. First, path coverage may not be adapted to the criteria under consideration. Second, some of the coverage requirements may be infeasible. Third, we need to be able to handle a large range of different coverage criteria. We propose three ingredients to tame these issues: a) a unified management of a large class of coverage criteria through labels (i.e. reachability objectives), b) a variant of DSE (denoted DSE*) designed to handle explicit coverage requirements at only a reasonable cost, c) and a combination of well-known static analysis (denoted VA+WP) for detecting infeasible coverage requirements. From a theoretical side, labels have been proved to emulate a large class of existing coverage criteria, DSE* prevents the exponential blowup of the search space induced by the standard (instrumentation-based) DSE approach to coverage-oriented testing, and VA+WP provides a sound detection of infeasible coverage requirements. From a practical side, these results have been implemented in the LTest plugin of the open-source software analyzer Frama-C. Experiments demonstrate that DSE* performs significantly better than DSE when considering coverage requirements, and that VA+WP is able to achieve a near-complete detection of infeasible coverage requirements. Altogether, LTest is a powerful software testing toolset, providing coverage estimation, test generation and infeasibility detection for a large class of coverage criteria. This talk is based on recent publications at ICST 2014, TAP 2014 and ICST 2015.
  • 15h45 : Salim Perchy (LIX)
On the Operations of Spacing and Extruding Information
Abstract: We take a look at the concept of space and the movement of information across spaces in algebraic structures. We formalize this concept as an operation over elements in constraint systems. Here, the elements represent assertions (i.e. temperature > 20) which in turn can be interpreted as partial information of the systems being modeled. Movement of information is also defined as an operation over the same elements, we call it ‘extrusion’. We study the properties of extrusion and its relation to spaces in constraint systems. We use this new mathematical formalism to give semantics to a bimodal logic where the space and extrusion operators are interpreted as belief and utterance modalities. This interpretation is in line with the epistemic nature of applications that analyze behavior such as opinions and lies.
KEYWORDS: Epistemic logics, Constraint programming, Knowledge and Lies
  • 16h15 : Sylvain Legay
Tropical homomorphism problems and their connections with constraint satisfaction problems
Abstract : This talk presents our results obtained in searching for a dichotomy of (H,c)-COLORING problems, aka tropical homomorphism problems. The main result is that existence of such a dichotomy is equivalent to the existence of a dichotomy of Constraint Satisfaction Problems (CSP), the latter being a conjecture that has received considerable attention but not yet resolved. We have also studied the complexity of this problem for certain specific graph families.
  • 16.30 : Break
  • 17.00/ 18.00 : Presentations of GTs (Working Groups)
OVSTR (Optimizing Real-Time Systems) - Florian Brandner
SHY (Hybrid Systems) - Alexandre Chapoutot
SASEFOR (Formal Methods) - Hubert Comon-Lundh