Ph.D. Course on Symbolic Execution, VT'21

Background

During spring, we will conduct a PhD course or reading group on symbolic execution techniques. Our immediate motivation is that symbolic execution is a key technique in many software verification, testing, and fuzzing approaches, but there are also many other potential usages. Symbolic execution was conceived already in the 1970's but has become increasingly powerful and used in the last 10-20 years.

Aim

The aim of the course is threefold

Cover basic theory and techniques for symbolic execution
Cover (mostly rather recent) approaches to different aspects related to symbolic execution (difficulties, extensions, applications, ...)
Make participants able to implement symbolic techniques for some useful purpose.

Organization

The foreseen organization will have three parts, corresponding to the aims

lectures/reading on basic theory and techniques
- Lectures can be found on internet, complemented by papers/book chapters
Presentation and discussion of specialized papers.
- In each meeting, one participant will present a paper, followed by critique and discussion.
- Each participant will be responsible for X presentations, and make written reviews on Y papers, where Y is larger than X.
- This part could be organized analogously to a PC review process, where each paper has a lead reviewer and two extra reviewers.
- Whole course https://www.youtube.com/channel/UCvwqRhlkE_Wm2FF9qzvHfJw - DSE lecture https://www.youtube.com/watch?v=UhtUyTJ-P2c
A mini-project which involves implementation of symbolic execution techniques, or use of an existing such implementation.
- Each participant chooses a project that is in line with his/her interests.

Preliminarily, we can offer 5-10 credits, where parts 1 and 2 together 5 credits, and the project's credits can be flexible: depending on its size.

Material

This page is a preliminary list of material. You are invited to comment and add your preferred papers or basic course material.

Schedule:

The course will run in Zoom 64271619437 (https://uu-se.zoom.us/j/64271619437) on Wednesdays, 15.15 - 17.00, starting February 10. Preliminary outline for first lectures

Feb. 10, 15-17 Intro, overview and organization:
Organization of the course slides
Basic ideas of Symbolic Execution, based on the paper A survey of Symbolic Exectuion Techniques, partially based on slides by Emilio Coppa and slides by Hakjoo Oh. The paper defines key challenge areas for SE: (1) Modeling memory, (2) Environment interaction, (3) Path explosion, (4) Constraint solving, each of which should be treated in (at least) one paper session.
Feb. 17, 15-17 Constraint Solving (1) slides and Scala code
Feb. 24, 15-17 Dynamic Symbolic Execution,
party using slides from Lecture 11 of Rightingcode.org, and if time permits, to summarize Godefroid, P., Levin, M. Y., Molnar, D. 2008. Automated whitebox fuzz testing. If time permits, we will do a DSE engine in Scala. Here is some suggested code.
March 3, 15-17 Constraint Solving (2) slides, and notes.
March 10, 15-17 LLVM and Klee (1) material (by Hooman Asadian) and video.
March 17, 15-17 LLVM and Klee (2) example programs, slides
March 24 No meeting
March 31, 15-17 Paper presentation (by Hooman Asadian): Systematic comparison of symbolic execution systems: intermediate representation and its generation. S Poeplau, A Francillon
April 7, 15-17 Guest Lecture: Kostis Sagonas: Concolic testing of higher-order functional languages
Abstract:
Concolic testing is a fully automatic software testing technique that combines concrete and symbolic execution of a program unit in an attempt to explore all the code paths in this unit. In this talk, we will describe how concolic testing can be applicable to high-level languages in general and to functional programming languages in particular. For such languages, the concolic engine needs to efficiently support pattern matching, recursive data types such as lists, recursion and higher-order functions. We will also briefly talk about the engineering effort that concolic testing tools require, in particular in interfacing with SMT solvers.
April 14 - June 9 Paper presentations (see below schedule)

Paper Presentations:

Date	Presenter	No	Title and Authors	Reviewers
March 31	Hooman Asadian:	19	Systematic comparison of symbolic execution systems: intermediate representation and its generation. S Poeplau, A Francillon	A. El Yaacoub, Z. Esen
April 14	Ahmed El Yaacoub:	15	Assertion guided symbolic execution of multithreaded programs. S Guo, M Kusano, C Wang, Z Yang, A Gupta	M. El Abdellaoui, S. Das
April 21	Sarbojit Das:	13	Con2colic testing. A Farzan, A Holzer, N Razavi, H Veith	S. Grahn, M. Lång
April 28	Samuel Grahn:	14	Symbolic execution of multithreaded programs from arbitrary program contexts. T Bergan, D Grossman, L H Ceze	N. Huber, M. Lång
May 5	Nikolaus Huber:	23	JDART: A Dynamic Symbolic Analysis Framework	A. El Yaacoub, A. Stjerna
May 12	Amanda Stjerna:	18	Symbolic execution with SymCC: Don't interpret, compile! S Poeplau and A Francillon,	H. Asadian, N. Huber
May 19	Zafer Esen:	7	Kenneth L. McMillan: Lazy Annotation for Program Testing and Verification	S. Das, C. Poncelet
May 26	Meriame El Abdellaoui:	11	Constraint Programming for Dynamic Symbolic Execution of JavaScript. R Amadini, M Andrlon, G Gange etal.	Z. Esen, C. Poncelet
Jun 2	Clement Poncelet:	3	Efficient State Merging in Symbolic Execution. V Kuznetsov, J Kinder, S Bucur, G Candea	M. El Abdellaoui, A. Stjerna
Jun 9	Magnus Lång:	8	Memory models in symbolic execution: key ideas and new thoughts. L Borzacchiello, E Coppa, D Cono D'Elia, C Demetrescu	H. Asadian, S. Grahn

Homework Exercises

Write SE-analyzer for arrays

How to Sign Up (OLD Info):

The course is planned to run 2hrs/week, starting the week of Feb. 8. A You sign up by indicating your possible slots in the week on the doodle https://doodle.com/poll/mwcd468a49b8mbzm. Do this before January 27.

Most welcome
Bengt Jonsson and Philipp Rümmer