Seminar Topics: Winter Semester 2017/18
The list below is not final yet. Topics will still be added or removed, supervisors might change, but the list below might give you an idea of what you can expect in the seminar.
Please note that PDFs for some papers are only accessible via the university network.
The goal of this seminar topic is to explain the basic architecture of SMT (Satisfiability modulo theories) solvers and illustrate a use case for an SMT solver based on an example.
- Leonardo Mendonça de Moura, Nikolaj Bjørner:
Satisfiability modulo theories: introduction and applications.
Commun. ACM 54(9):
- Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli:
Satisfiability Modulo Theories.
Handbook of Satisfiability 2009
Generating verification conditions
SMT-solvers can be used to verify the correctness of programs. To do this, programs with their specification have to be translated into logical formulas. The goal of this topic is to explain how this can be done by calculating “weakest preconditions”.
- K. Rustan M. Leino:
Efficient weakest preconditions.
Information Processing Letters 93.6 (2005)
- Michael Barnett, K. Rustan M. Leino:
Weakest-precondition of unstructured programs.
The Dafny and Boogie verification tools
In this topic the concrete verification tool “Dafny” (and its backend “Boogie”) should be presented. The focus here should be on explaining how the a concrete tool can be used to verify program. In particular the verification of programs with loops and procedures shall be explained using suitable examples.
- Dafny: A Language and Program Verifier for Functional Correctness
- Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, K. Rustan M. Leino:
Boogie: A Modular Reusable Verifier for Object-Oriented Programs.
- K. Rustan M. Leino:
Dafny: An Automatic Program Verifier for Functional Correctness.
LPAR (Dakar) 2010
The Chalice verification tool
Chalice is a programming language and program verifier for concurrent program. The focus for this seminar should be on explaining the techniques used by Chalice for verifying concurrent programs, in particular the concepts of framing and permissions.
- Chalice Homepage
- K. R. M. Leino and P. Müller:
A Basis for Verifying Multi-Threaded Programs
European Symposium on Programming (ESOP), 2009
- K. R. M. Leino, P. Müller, and J. Smans:
Verification of Concurrent Programs with Chalice Foundations of Security Analysis and Design V, 2009.
Property based testing
The goal of this topic is to explain, how a specification can be checked through testing instead of verification. This shall be explained based on the Haskell libraries “QuickCheck” and “SmallCheck”, which use random testing and bounded enumeration of inputs.
- Koen Claessen, John Hughes:
QuickCheck: a lightweight tool for random testing of Haskell programs.
- Colin Runciman, Matthew Naylor, Fredrik Lindblad:
Smallcheck and lazy smallcheck: automatic exhaustive testing for small values.
This topic is about a smarter approach to property based testing, where different inputs are explored using symbolic executing. The goal here is to explain symbolic execution and how it is used to explore different executions of the program in testing.
- Patrice Godefroid, Nils Klarlund, Koushik Sen:
DART: directed automated random testing.
- Cristian Cadar, Dawson R. Engler:
Execution Generated Test Cases: How to Make Systems Code Crash Itself.
- Koushik Sen, Darko Marinov, Gul Agha:
CUTE: a concolic unit testing engine for C.
ESEC/SIGSOFT FSE 2005
- Aggelos Giantsios, Nikolaos S. Papaspyrou, Konstantinos Sagonas:
Concolic testing for functional languages.
For this topic, the basics of model checking should be explained. In particular, it should be explained, how model checking can be used to verify programs using the Java PathFinder tool as an example.
- Klaus Havelund, Thomas Pressburger:
Model Checking JAVA Programs using JAVA PathFinder.
International Journal on Software Tools for Technology Transfer
- Gerard J. Holzmann:
The model checker SPIN
IEEE Transactions on Software Engineering (TSE)
- Christel Baier, Joost-Pieter Katoen:
Principles of model checking
- K. C. Sivaramakrishnan, Gowtham Kaki, Suresh Jagannathan:
Declarative programming over eventually consistent data stores.
- Leslie Lamport:
Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers.
- Chris Newcombe:
Why Amazon Chose TLA +.
- Concuerror: Systematic concurrency testing tool for Erlang programs.
- Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, Konstantinos F. Sagonas:
Optimal dynamic partial order reduction.
The goal of this seminar topic is to explain the basic ideas of session types based on the language Scribble.
- Kohei Honda, Nobuko Yoshida, Marco Carbone:
Multiparty Asynchronous Session Types.
Journal of the ACM, Volume 63
- Nobuko Yoshida, Raymond Hu, Rumyana Neykova, Nicholas Ng:
The Scribble Protocol Language.
- Ryan Stutsman, Collin Lee, John K. Ousterhout:
Experience with Rules-Based Programming for Distributed, Concurrent, Fault-Tolerant Code.
USENIX Annual Technical Conference 2015
The goal here is to explain the protocol behind Blockchains, which are used in crypto-currencies such as Bitcoin. Moreover the distinction between Proof-of-Work vs. BFT replication should be explained and usages of Blockchain protocols beyond crypto-currencies should be researched and explained.
- Satoshi Nakamoto:
Bitcoin: A Peer-to-Peer Electronic Cash System.
- Marko Vukolic:
The Quest for Scalable Blockchain Fabric: Proof-of-Work vs. BFT Replication.
- Ittay Eyal, Adem Efe Gencer, Emin Gün Sirer, Robbert van Renesse:
Bitcoin-NG: A Scalable Blockchain Protocol.
- Etherum (White Paper)
- Todd Warszawski, Peter Bailis:
ACIDRain: Concurrency-Related Attacks on Database-Backed Web Applications.
SIGMOD Conference 2017
Serializability for eventual consistency
- Lucas Brutschy, Dimitar Dimitrov, Peter Müller, Martin T. Vechev:
Serializability for eventual consistency: criterion, analysis, and applications.
- Peter Alvaro, Joshua Rosen, Joseph M. Hellerstein:
Lineage-driven Fault Injection.
SIGMOD Conference 2015
Generalized Isolation Level Definitions
- Atul Adya, Barbara Liskov, Patrick E. O’Neil:
Generalized Isolation Level Definitions.
Client-Centric Specification of Database Isolation
- Natacha Crooks, Youer Pu, Lorenzo Alvisi, Allen Clement:
Seeing is Believing: A Client-Centric Specification of Database Isolation.