Seminar in Theoretical CS, Summer Semester 2015
News
- 16.06.2015: presentation template added
- 14.04.2015: assignment of topics completed
- 10.04.2015: report template added
- 09.04.2015: introductory slides added
- 18.02.2015: assignment of supervisors completed
- 13.01.2015: we are online
Deadlines
| 09.04.2015, 13:00 | Introduction at seminar room of i2 (E1, room 4201b) |
| 18.05.2015 | Detailed outline due |
| 01.06.2015 | Report due |
| 15.06.2015 | Final version of report due |
| 29.06.2015 | Slides due |
| 06.07.2015 | Final version of slides due |
| 13./14.07.2015 | Seminar at seminar room of i2 (E1, room 4201b) |
Overview
This seminar addresses several aspects of programming languages and systems, with emphasis on how principles underpin practical applications. Here the notion of “programming languages and systems” has to be understood in a broad sense; it ranges from sequential programming languages over concurrent and probabilistic systems to logical approaches such as model checking.
Each area features a number of topics which are each covered by a scientific journal or conference article (please refer to the references below). These research articles are the basis on which students have to prepare their report and presentation.
Prerequisites
Basic knowledge in the following areas is expected:
- Formal languages and automata theory
- Mathematical logic
- Previous knowledge in semantics of programming languages, program analysis, model checking and/or concurrency theory is helpful but not mandatory
Topics
Program Analysis
- Quantitative Interprocedural Analysis
- Literature: Krishnendu Chatterjee, Andreas Pavlogiannis, Yaron Velner: Quantitative Interprocedural Analysis. POPL 2015, 539-551
- Supervisor: Kevin van der Pol
- Student: Moumen Elteir
- Interprocedural Analysis with Callbacks
- Literature: Hao Tang, Xiaoyin Wang, Lingming Zhang, Bing Xie, Lu Zhang, Hong Mei: Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks. POPL 2015, 83-95
- Supervisor: Thomas Noll
- Student: Petro Tarasenko
- Abstraction Refinement
- Literature: Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan: Abstractions from proofs. POPL 2004, 232-244
- Supervisor: Thomas Noll
- Student: Momchil Marinov
Model Checking
- Partial Order Reduction
- Literature: Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, Konstantinos F. Sagonas: Optimal dynamic partial order reduction. POPL 2014, 373-384
- Supervisor: Tim Lange
- Student: Ivan Vatov
- Bounded Model Checking
- Literature: Javier Esparza, Pierre Ganty, Rupak Majumdar: A Perfect Model for Bounded Verification. LICS 2012, 285-294
- Supervisor: –
- Student: –
- Software Model Checking via IC3
- Literature: Alessandro Cimatti, Alberto Griggio: Software Model Checking via IC3. CAV 2012, LNCS 7358, 277-293
- Supervisor: Tim Lange
- Student: Thomas Mertens
Probabilistic Systems
- Probabilistic Termination
- Literature: Luis María Ferrer Fioriti, Holger Hermanns: Probabilistic Termination: Soundness, Completeness, and Compositionality. POPL 2015, 489-501
- Supervisor: Benjamin Kaminski
- Student: Simon Feiden
- Abstract Semantics of Probabilistic Programs
- Literature: Neil Toronto, Jay McCarthy, David Van Horn: Running Probabilistic Programs Backwards. ESOP 2015, to appear
- Supervisor: –
- Student: –
- Slicing Probabilistic Programs
- Literature: Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, Selva Samuel: Slicing probabilistic programs. PLDI 2014, 133-144
- Supervisor: Federico Olmedo
- Student: Sindhu Aitharaju
- Analysis of Markov Decision Processes
- Literature: Serge Haddad, Benjamin Monmege: Reachability in MDPs: Refining Convergence of Value Iteration. Reachability Problems 2014: 125-137
- Supervisor: Christian Dehnert
- Student: Alexandra Dalevskaya
- Probabilistic Automata on Finite Words
- Literature: Hugo Gimbert, Youssouf Oualhadj: Probabilistic Automata on Finite Words: Decidable and Undecidable Problems. ICALP 2010, LNCS 6199, 527-538
- Supervisor: –
- Student: –
Concurrent Systems
- Verification of Multithreaded Programs
- Literature: Javier Esparza, Pierre Ganty, Tomás Poch: Pattern-Based Verification for Multithreaded Programs. ACM Trans. Program. Lang. Syst. 36(3): 9 (2014)
- Supervisor: –
- Student: –
- Linearisability of Concurrent Data Structures
- Literature: Gerhard Schellhorn, John Derrick, Heike Wehrheim: A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. ACM Trans. Comput. Log. 15(4): 31 (2014)
- Supervisor: Xiaoxiao Yang
- Student: Nikola Velinov
- Quantitative Quiescent Consistency
Separation Logic
- Complexity of Deciding Entailment
- Literature: Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max I. Kanovich, Joël Ouaknine: Foundations for Decision Problems in Separation Logic with General Inductive Predicates. FoSSaCS 2014: 411-425
- Supervisor: Christoph Matheja
- Student: Frank Emrich
- Deciding Satisfiability
Schedule of Talks
| Monday 13.07.2015 | |
|---|---|
| 09:00-10:30 | 1, 10 |
| 10:45-12:15 | 2, 3 |
| 13:30-15:00 | 4, 6 |
| Tuesday 14.07.2015 | |
| 13:15-14:45 | 7, 9 |
| 15:00-16:30 | 13, 15 |
Additional Material
Registration
Registration to the seminar is handled between January 14 and 28, 2015, via the central online form.
Contact
Thomas Noll <noll at cs.rwth-aachen.de>