USE 2015 - 1st Usages of Symbolic Execution 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, verification, model checking, debugging
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