1st  Usages of Symbolic Execution Workshop USE'15

In conjunction with FM 2015 (Oslo, 22-26 June 2015)

Co-located with FM 2015

USE'15 is an half-day workshop scheduled on Tuesday 23.

SETS and USE workshops join their forces to propose a full day program.

Preliminary program:

9:00 - 9:15  Opening

9:15 - 10:00 Invited talk
Symbolic Execution and Advanced Test Coverage Criteria
Nikolaï Kosmatov

Abstract : Automatic test data generation (ATG) is a major topic in software engineering. In this talk, we try to bridge the gap between the coverage criteria supported by state-of-the-art white-box ATG techniques, especially Dynamic Symbolic Execution, and advanced coverage criteria found in the literature. We define a new coverage criterion, label coverage, and prove it to be both expressive and amenable to efficient automation. We propose several innovative techniques resulting in an effective black-box support for label coverage, while a direct approach induces an exponential blow-up of the search space. Experiments show that the proposed optimizations yield very significant savings, allowing to lift ATG to label coverage with only a slight overhead. This is a joint work with Sébastien Bardin, Omar Chebaro and Mickaël Delahaye.

10:00 - 10:30 Coffee break

10:30 - 11:00
Test Data Generation for Cyclic Executives with CBMC and Frama-C : A Case Study
Omer Landry Nguena Timo and Guillaume Langelier

11:00 - 11:30
Symbolic Input-Output Conformance Checking for Model-Based Mutation Testing
Bernhard K. Aichernig and Martin Tappler

11:30 - 12:00
An Illustrative Use Case of the DIVERSITY Platform based on UML Interaction Scenarios
Mathilde Arnaud, Boutheina Bannour and Arnault Lapitre

12:00 - 12:30
Bound Analysis for Whiley Programs
Min-Hsien Weng, Mark Utting and Bernhard Pfahringer

12:30 - 14:00 Lunch

14:00 - 17:00 SETS workshop

USE 2015

Symbolic execution was first defined for programs during the 70th as a way to analyze feasible paths of programs under analysis and also, conjointly with solving techniques, to generate test cases for partition structural testing. The underlying concept consists in executing programs, not for concrete numerical values but for symbolic parameters, and computing logical constraints on those parameters at each step of the execution. The scope of programming languages that can be analyzed by tools with this technique has been extended during the following decades, and more recently this technique has been transposed at the modeling level, to analyze possible executions of models written using various modelling languages.

Symbolic execution allows computing program or model semantics and representing them efficiently in an abstract manner.  As such they form a very interesting basis to build formal methods upon them. Symbolic execution has been used as a base for implementing structural testing or model based testing algorithms, refinement testing, model or program debugging techniques (deadlock search, invariant checking), model-checking introducing first order structure. The growing interest on symbolic execution, inducing a growing community of users, is also motivated by the fact that the scalability of this technique has increased thanks to recent advances that have been made in constraint solving techniques.

Even though the number of contributors to symbolic execution techniques and the number of users increase, the different communities working with this technique do not have a common place to share both about the next steps to achieve in terms of, data structure treatments, mixing with other formal techniques, usage scenarios such as embedding the usage of symbolic techniques in some design processes, feedbacks on case studies, scalability…

USE aims at being a forum to cover those needs, both for researchers working in the scope of formal techniques and grounding their analysis techniques on symbolic execution, and for users of technologies based on symbolic execution. 

Topics include but are not limited to:

Important dates:

Full paper due: 10 April 2015 (updated)

Notification: 10 May 2015 (updated)

Camera-ready: 1 June 2015

Workshop'day: 23 June 2015

Submission guidelines:

Authors may apply by sending a paper (6-15 pages) in English describing their contribution. The paper should contribute to the discussion of the topics of the workshop. Position papers, work-in-progress, surveys are also welcome.

Papers must be written in English, not exceed 15 pages and be conforming to the ENTCS's latex
format (http://www.entcs.org/prelim.html).

The proceedings of the workshop will be published by ENTCS

Accepted papers will be distributed to the attendees in the workshop proceedings.

Submissions can be made here. If you experiment problems to submit via easychair, please send us directly your contributions by email at pascale.legall@ecp.fr and christophe.gaston@cea.fr.

Organizing Committee:

Christophe Gaston (CEA LIST – France): christophe.gaston@cea.fr

Pascale Le Gall (Ecole Centrale Paris – France): pascale.legall@ecp.fr

Alexandre Petrenko (CRIM – Canada): alexandre.petrenko@crim.ca

Program Committee:

Sébastien Bardin (CEA LIST)

Francis Bordeleau (Ericsson)

Juergen Dingel  (Queen’s University)

Vijay Ganesh (Waterloo University)

Christophe Gaston (CEA LIST)

Arnaud Gotlieb (Simula Research Laboratory)

Thierry Jéron (IRISA Rennes)

Pascale Le Gall (ECP)

Delphine Longuet (Université Paris Sud)

Alexandre Petrenko (CRIM)

Nicolas Rapin (CEA LIST)

Koushik Sen (University of California, Berkeley)

Jan Tretmans (TNO - Embedded Systems Innovation)


Pascale Le Gall   pascale.legall@ecp.fr