USE 2018 @ ICST 2018
The Second International Workshop on Usages of Symbolic Execution (USE 2018)
April 9, 2018,Västerås, Sweden
Contact : firstname.lastname@example.org
USE 2018 is colocated with
the 11th IEEE Conference on Software Testing, Verification and Validation (ICST 2018)
April 9 -13, 2018
Aros Congress Center
Workshop date : April 9, 2018
Session 1 9:00-10:30 (invited talks)
Generating Heap Test Inputs with Symbolic Execution — Mauro Pezzè
Symbolic Execution for the Security Realm: the Cyber Grand Challenge Story — Emilio Coppa
Session 2 11:00-12:30 (regular talks)
Automatic Testing of Symbolic Execution Engines — Timotej Kapus and Cristian Cadar
Symbolic Execution and Code-Coverage Oriented Testing — Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov, Mickaël Delahaye, Virgile Prevosto
DIVERSITY : An Extensible Symbolic Execution Tool — Boutheina Bannour and Arnault Lapitre
Session 3. 14:00-15:30 (invited talk)
Using Test Ranges to Enhance Symbolic Execution — Sarfraz Khurshid
Test generation from FSM fault model by Constraint Solving — Omer Nguena-Timo
Session 4. 16:00-17:30 (regular talks)
Symbolic execution for binary-level security — Sébastien Bardin and Richard Bonichon
Synthesizing Adapters For Binary Code Using Symbolic Execution — Vaibhav Sharma and Stephen McCamant
Confirmed invited speakers
Emilio Coppa Sapienza University of Rome
Symbolic Execution for the Security Realm: the Cyber Grand Challenge Story
Abstract: Symbolic execution techniques have evolved significantly in the last decade, with notable applications to compelling problems from several domains like software testing, security, and code analysis. This trend has not only improved existing solutions, but also led to novel ideas and, in some cases, to major practical breakthroughs. For instance, the push for scalable automated program analyses in security has culminated in the 2016 DARPA Cyber Grand Challenge (CGC), which hosted systems for detecting and fixing vulnerabilities in unknown software with no human intervention, such as angr and Mayhem, that competed for nearly $4M in prize money. In this talk we walk through the symbolic execution frameworks that have been used by some of the finalists in the DARPA CGC, pinpointing prominent research aspects and discussing interesting future directions.
Sarfraz Khurshid University of Texas at Austin
Using Test Ranges to Enhance Symbolic Execution
Abstract: The impact of robust and effective bug-finding systems based on symbolic execution has received increased recognition, establishing symbolic execution as the premier analysis for systematic checking in many domains. This talk focuses on the concept of test ranges that were initially defined for distributing symbolic execution to reduce its cost, and later developed for memoizing and integrating symbolic execution to increase its applicability and usefulness. The talk also presents how using test ranges generalizes beyond symbolic execution to enhance a few other analyses that share the spirit of systematic exploration.
Mauro Pezzè Università della Svizzera italiana, Lugano
Generating Heap Test Inputs with Symbolic Execution
Abstract: Generating test inputs has been a primary application of symbolic execution since the early studies. In their seminal work of the seventies, both King and Clark addressed the problem of generating test cases for programs with inputs of simple data types, by computing and solving path conditions. At the turn of the millennium, Khurshid, Pasareanu and Visser introduced lazy initialisation to deal with expressions on complex data structures, an effective but inefficient way of working with complex data structures, thus opening a popular research direction. At the same time, the newly born discipline of search based software engineering started focusing on the automated generation of concrete test inputs with impressive results. This talk will briefly recall the main milestones of generating test inputs with symbolic execution, will extensively discuss the combination of lazy-initialization-inspired techniques with search-based software engineering to efficiently generate concrete test cases form programs with complex heap inputs, and will outline the promising future industrial and research directions of the discipline.
Omer Nguena-Timo CRIM – Computer Research Institute of Montreal
Test generation from FSM fault model by Constraint Solving
Abstract: Testing aims at revealing faults in systems. A fault model specifying the faults to be detected could be used for test generation. In this talk we present test generation methods for complete fault coverage of fault models of systems represented with finite state machines. A fault model represents a sheer number of possible (faulty) implementations. The method is based on constraint solving and avoids one-by-one enumeration of the implementations. We present experimental results obtained with a prototype tool and an industrial-like model of system.
Symbolic execution was originally defined for programs in the 1970s as a way to analyze feasible paths of programs under analysis and, jointly with solving techniques, to generate test cases for partition structural testing. The scope of programming languages that can be analyzed by tools based on this technique has been extended during the following decades. Symbolic execution has been transposed at the modeling level, to analyze possible executions of models in 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.
Although the number of contributors to symbolic execution techniques and the number of its users increase, the different communities working with this technique do not have a common place to share ideas, discuss new challenges, future developments, other usage scenarios, feedbacks on case studies, scalability… USE aims at being a forum to cover those needs, both for researchers and practitioners working on symbolic execution and its applications.
USE 2018 is aimed at encouraging the exchange of ideas and discussions between participants interested in symbolic execution and related topics. USE 2018 will be organized around several invited talks given by experts of the considered domains, several accepted talks based on a lightweight reviewing of submitted extended abstracts, and will feature space for questions and discussions.
Topics of interests
They include (but are not restricted 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 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…),
- Synergies between constraint solving techniques and symbolic execution,
- Case studies, tools and benchmarks.
The USE workshop topics are highly relevant to ICST audience since many V&V approaches and tools rely on symbolic execution. Thus ICST will be a perfect venue for the USE workshop for discussing recent improvements, optimizations, experiments and tools as well as future challenges and perspectives related to symbolic execution and its applications.
Call for contributions
All interested participants are invited to submit an abstract of a talk to be presented during the workshop. Talks may present both original or already published work, tool developments, experience reports, position papers as well as work in progress. Talks with emphasis on novel ideas or challenges are particularly welcome. Abstracts of at most three pages (excluding references), in PDF form, can be submitted by use2018 at cea.fr.
Publications. No official publication of proceedings is planned. The presentations will be posted on the workshop website to share between participants and for future reference.
The workshop will deliver a « best presentation award » to the best commucation during the workshop.