2nd  Usages of constraint Solving

and symbolic Execution Workshop

USE'16

In conjunction with FM 2016 (Limassol, Cyprus, 7-11 November 2016)

Co-located with FM 2016





USE 2016

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 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. The growing interest on symbolic execution 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.

Constraint solving can be regarded as the key-enabling technology for symbolic execution as it leverages the automated analyses of path conditions. However, it must be understood that using constraint solvers as black-boxes in that context simply does not work as programming (or modelling) languages features complicate the treatment and analysis of program (or model) paths. Since twenty years, a tremendous effort has been made to tune existing solvers (SAT, SMT, CP, ILP,…) or to create new dedicated solvers for that purpose. 



USE aims at being a forum both for researchers working in the scope of formal techniques and grounding their analysis techniques on symbolic execution and/or constraint solving, and for users of technologies based on those techniques.
Papers addressing only one of the two techniques will be welcomed so that both communities can take benefit of the most recent breakthroughs of the two domains.

Topics include but are not limited to:


Important dates:



Full paper due:  1 September 2016

Notification: 30 September 2016

Camera-ready: 20 October 2016

Workshop'day: 7-11 November 2016


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 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 (using Easychair facilities). If you experiment problems to submit via easychair, please send us directly your contributions by email at pascale.legall@centralesupelec.fr


Organizing Committee:

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

Arnaud Gotlieb Gotlieb (SIMULA Research Laboratory – Norway): arnaud@simula.no


Pascale Le Gall (CentraleSupélec – France):
pascale.legall@centralesupelec.fr

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

Program Committee:


Boutheina Bannour (CEA LIST, France)

Armin Biere (Johannes Kepler University, Austria)

Sébastien Bardin (CEA LIST, France)

Juergen Dingel (Queen’s University, Canada)

Vijay Ganesh (Waterloo University, Canada)

Thierry Jéron (INRIA, France)

Pascale Le Gall (CentraleSupélec, France)

Michael Leuschel (University of Düsseldorf, Germany)

Delphine Longuet (Université Paris Sud,France)

Michel Rueher (Université de Nice, France)


Contact:

Pascale Le Gall   pascale.legall@centralesupelec.fr