Research Topics in Software Engineering

Overview

The main goal of this seminar is to introduce students to the latest research trends in the field of programming languages and systems, including:

Core automated program analysis and synthesis techniques (e.g., new algorithms, combinations with machine learning).
Inter-disciplinary applications of these techniques to a variety of challenges in system reliability, security and performance (e.g., reasoning about networks).

The seminar is carried out as a set of presentatins (2 each lecture) chosen from a set of available papers (available below). The grade is determined as a function of the presentation, handling questions and answers, and participation.

Presentation Schedule

Date	Title	Presenter	Advisor
Feb 22	Introduction to the seminar (topics, objectives, structure)	Prof. Dr. Martin Vechev
Mar 7	A Static Analyzer for Large Safety-Critical Software	Dario Bösch	Gagandeep Singh
	A User-Guided Approach to Program Analysis	Serge Balzan	Pavol Bielik
Mar 14	Proving that programs eventually do something good	Romy Profanter	Dr. Sasa Misailovic
	Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses	Simon Fritsche	Gagandeep Singh
Mar 21	ArMOR: defending against memory consistency model mismatches in heterogeneous architectures	Oliver Butz	Andrei Dan
	Set-based pre-processing for points-to analysis	Balz Guenat	Veselin Raychev
Apr 4	Proving non-termination	Parthasarathy Gaurav	Dr. Sasa Misailovic
	A systematic study of automated program repair: Fixing 55 out of 105 bugs for $8 each	Nino Weingart	Dr. Sasa Misailovic
Apr 11	Continuity analysis of programs	Simon Wehrli	Timon Gehr
	SPEED: Precise and Efficient Static Estimation of Program Computational Complexity	Stefan Blumer	Timon Gehr
	Transforming Spreadsheet Data Types using Examples	Madelin Schumacher	Veselin Raychev
Apr 25	Learning a Strategy for Adapting a Program Analysis via Bayesian Optimisation	Maximilian Wurm	Veselin Raychev
	Learning tractable probabilistic models for fault localization	Santhanam Prabhakaran	Veselin Raychev
	Rethinking serializable multiversion concurrency control	Ștefan Irimescu	Dimitar Dimitrov
May 2	FastTrack: Efficient and Precise Dynamic Race Detection	Lukas Kuster	Pavol Bielik
	Oracle guided component-based program synthesis	Pascal Roos	Pavol Bielik
	Producing wrong data without doing anything obviously wrong!	Florian Buenzli	Dr. Sasa Misailovic
May 9	Precise and Efficient Static Array Bound Checking for Large Embedded C Programs	Pavle Djordjevic	Gagandeep Singh
	Declarative fence insertion	Benjamin Mularczyk	Andrei Dan
May 23	Finding Deep Compiler Bugs via Guided Stochastic Program Mutation	Tobias Krebs	Prof. Dr. Patrick Lam
	Interactively verifying absence of explicit information flows in Android apps	Samuel Ueltschi	Prof. Dr. Patrick Lam
	The SeaHorn Verification Framework	Thomas Betschart	Gagandeep Singh
May 30	COZ: finding code that counts with causal profiling	Marcel Mohler	Pavol Bielik
	Configurable software verification: concretizing the convergence of model checking and program analysis	Johannes Baum	Gagandeep Singh

Candidate Papers

Some of the papers below are available through ACM Digital Library which can be accessed using nethz credentials.

Program Analysis
Precise and Efficient Static Array Bound Checking for Large Embedded C Programs	PLDI 2004
Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses	SCP 2009
A Static Analyzer for Large Safety-Critical Software	PLDI 2003
Configurable software verification: concretizing the convergence of model checking and program analysis	CAV 2007
The SeaHorn Verification Framework	CAV 2015
Continuity analysis of programs	POPL 2010
Set-based pre-processing for points-to analysis	OOPSLA 2013
SPEED: Precise and Efficient Static Estimation of Program Computational Complexity	POPL 2009
Proving that programs eventually do something good	POPL 2007
A User-Guided Approach to Program Analysis	FSE 2015
The Complexity of Interaction	POPL 2016

Concurrency and Verification
Declarative fence insertion	OOPSLA 2015
Trading Fences with RMRs and Separating Memory Models	PODC 2015
ArMOR: defending against memory consistency model mismatches in heterogeneous architectures	ISCA 2015
SATCheck: SAT-Directed Stateless Model Checking for SC and TSO	OOPSLA 2015
FastTrack: Efficient and Precise Dynamic Race Detection	PLDI 2009
Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components	POPL 2016
Rethinking serializable multiversion concurrency control	VLDB 2015

Program Synthesis and Statistical Learning
Learning tractable probabilistic models for fault localization	AAAI 2016
Synthesizing Piece-wise Functions by Learning Classifiers	TACAS 2015
Transforming Spreadsheet Data Types using Examples	POPL 2016
Learning a Strategy for Adapting a Program Analysis via Bayesian Optimisation	OOPSLA 2015
Oracle guided component-based program synthesis	ICSE 2010

Program Testing and Performance
Finding Deep Compiler Bugs via Guided Stochastic Program Mutation	OOPSLA 2015
Interactively verifying absence of explicit information flows in Android apps	OOPSLA 2015
A practical guide for using statistical tests to assess randomized algorithms in software engineering	ICSE 2011
Producing wrong data without doing anything obviously wrong!	ASPLOS 2009
Stabilizer: statistically sound performance evaluation	ASPLOS 2013
Proving non-termination	POPL 2008
A systematic study of automated program repair: Fixing 55 out of 105 bugs for $8 each	ICSE 2012
An analysis of patch plausibility and correctness for generate-and-validate patch generation systems	ISSTA 2015
COZ: finding code that counts with causal profiling	SOSP 2015