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
  1. Cover basic theory and techniques for symbolic execution
  2. Cover (mostly rather recent) approaches to different aspects related to symbolic execution (difficulties, extensions, applications, ...)
  3. Make participants able to implement symbolic techniques for some useful purpose.

Organization

The foreseen organization will have three parts, corresponding to the aims
  1. lectures/reading on basic theory and techniques
    • Lectures can be found on internet, complemented by papers/book chapters
  2. 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
  3. 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

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

Paper Presentations:

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

Homework Exercises

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