Research Topics in Software Engineering

Course no.
263-2100-00 S
Semester
Spring 2016
Lecturer
Prof. Dr. Martin Vechev
Head TA
Andrei Dan
EDoz
Link
Time
Monday, 4-6pm
Place
CHN D 48
Credits
2


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:

DateTitlePresenterSlidesAdvisor
Feb 22 Introduction to the seminar (topics, objectives, structure): PDF Prof. Dr. Martin Vechev
Mar 7 A Static Analyzer for Large Safety-Critical Software Dario Bösch PDF Gagandeep Singh
A User-Guided Approach to Program Analysis Serge Balzan PDF Pavol Bielik
Mar 14 Proving that programs eventually do something good Romy Profanter PDF Dr. Sasa Misailovic
Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses Simon Fritsche PDF Gagandeep Singh
Mar 21 ArMOR: defending against memory consistency model mismatches in heterogeneous architectures Oliver Butz PDF Andrei Dan
Set-based pre-processing for points-to analysis Balz Guenat PDF Veselin Raychev
Apr 4 Proving non-termination Parthasarathy Gaurav PDF 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 PDF Timon Gehr
Transforming Spreadsheet Data Types using Examples Madelin Schumacher PDF Veselin Raychev
Apr 25 Learning a Strategy for Adapting a Program Analysis via Bayesian Optimisation Maximilian Wurm PDF 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 PDF Pavol Bielik
Oracle guided component-based program synthesis Pascal Roos PDF Pavol Bielik
Producing wrong data without doing anything obviously wrong! Florian Buenzli PDF Dr. Sasa Misailovic
May 9 Precise and Efficient Static Array Bound Checking for Large Embedded C Programs Pavle Djordjevic PDF Gagandeep Singh
Declarative fence insertion Benjamin Mularczyk PDF Andrei Dan
May 23 Finding Deep Compiler Bugs via Guided Stochastic Program Mutation Tobias Krebs PDF Prof. Dr. Patrick Lam
Interactively verifying absence of explicit information flows in Android apps Samuel Ueltschi PDF Prof. Dr. Patrick Lam
The SeaHorn Verification Framework Thomas Betschart PDF Gagandeep Singh
May 30 COZ: finding code that counts with causal profiling Marcel Mohler PDF Pavol Bielik
Configurable software verification: concretizing the convergence of model checking and program analysis Johannes Baum PDF 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