1st Usages of Symbolic Execution Workshop USE'15
In conjunction with FM 2015
(Oslo, 22-26 June 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
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
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:
- Symbolic execution
for testing (white box / black box), consistency checking,
- Symbolic analysis of modelling and programming languages
- Taking into account complex data structure in symbolic execution processes
- Symbolic execution in the loop of design processes (e.g. refinement correctness assessment, model consistency checking, symbolic execution for dysfunctional analyses…)
- Coupling between constraint solving technics and symbolic execution
- Case study analysis
- Tools and benchmarks
Full paper due: 10 April 2015 (updated)
Notification: 10 May 2015 (updated)
Camera-ready: 1 June 2015
Workshop'day: 23 June 2015
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
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 firstname.lastname@example.org and email@example.com.
Pascale Le Gall (Ecole Centrale Paris – France): firstname.lastname@example.org
Alexandre Petrenko (CRIM – Canada): email@example.com
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)
Le Gall firstname.lastname@example.org