USE '16

2nd Workshop on Usages of constraint Solving and symbolic Execution

co-located with the 21th Int. Symposium on Formal Method FM'16

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. It 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 in order 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 of interest

• 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 languagesTaking into account complex data structure in symbolic execution and constraints techniques
• 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 techniques and symbolic execution
• Case studies, tools and benchmarks

Contact: pascale.legall@centralesupelec.fr