2nd Usages of constraint Solving
and symbolic Execution Workshop
In conjunction with FM
(Limassol, Cyprus, 7-11 November 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
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:
- Symbolic execution and/or constraints for
testing, consistency checking, verification, model checking, debugging
- Symbolic analysis and constraints for static and dynamic analyses of modelling and programming languages
- Taking into account complex data structure in symbolic execution and constraints technics
- Symbolic execution and constraint solving 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 studies, tools and benchmarks
Full paper due: 1 September 2016
Notification: 30 September 2016
Camera-ready: 20 October 2016
Workshop'day: 7-11 November 2016
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 firstname.lastname@example.org
Arnaud Gotlieb Gotlieb
(SIMULA Research Laboratory – Norway): email@example.com
Pascale Le Gall (CentraleSupélec – France): firstname.lastname@example.org
Alexandre Petrenko (CRIM – Canada): email@example.com
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)