Seminar in Theoretical CS, Winter Semester 2017/18

News

• 27.06.2017: we are online

Deadlines

Wed 11.10.2017, 14:00	Kick-off meeting at seminar room of i2 (building E1, room 4201b)
13.11.2017	Detailed outline of report due
11.12.2017	Full report due
15.01.2017	Presentation slides due
30./31.01.2018	Seminar talks at seminar room of i2 (building E1, room 4201b)

Overview

This seminar addresses several aspects of the design and (efficient and reliable) implementation of programming languages and systems, with emphasis on how principles underpin practical applications. Here the notion of “design and implementation” has to be understood in a broad sense; it ranges from parsing over static analysis techniques to code generation. The areas are oriented towards the annual Conference on Programming Language Design and Implementation, which is is the premier forum in the field of programming languages and programming systems research, covering the areas of design, implementation, theory, applications, and performance.

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 compiler construction, semantics of programming languages, or program analysis is helpful but not mandatory

Topics

Compilation

1. Adaptive LL(*) parsing
   • Literature:  http://dl.acm.org/citation.cfm?id=2660202 (OOPSLA 2014)
   • Supervisor: Matthias Volk
   • Student: Juri Schupilo
2. Counterexamples for bottom-up parsing conflicts
   • Literature:  http://dl.acm.org/citation.cfm?id=2737961 (PLDI 2015)
   • Supervisor: Matthias Volk
   • Student: Dustin Jungen
3. Verified compilation
   • Literature:  https://link.springer.com/chapter/10.1007/978-3-642-54833-8_7 (ESOP 2014)
   • Supervisor: Thomas Noll
   • Student: David Kraeutmann
4. Compilation of functional languages
   • Literature:  https://dl.acm.org/citation.cfm?id=3062380 (PLDI 2017)
   • Supervisor: Thomas Noll
   • Student: Raoul Schaffranek
5. Synthesis of machine code from semantics
   • Literature:  http://dl.acm.org/citation.cfm?id=2737960 (PLDI 2015)
   • Supervisor: Tim Lange
   • Student: Johannes Schulte
6. Improving accuracy for floating-point expressions
   • Literature:  http://dl.acm.org/citation.cfm?id=2737959 (PLDI 2015)
   • Supervisor: Sebastian Junges
   • Student: Niels Hendrik Wießner
7. Program enumeration for compiler testing
   • Literature:  http://dl.acm.org/citation.cfm?id=3062379 (PLDI 2017)
   • Supervisor: Sebastian Junges
   • Student: Alexander Bork

Analysis

8. Points-to analysis
   • Literature:  http://dl.acm.org/citation.cfm?id=3062360 (PLDI 2017)
   • Supervisor: Christina Jansen
   • Student: Daniel Cloerkes
9. Polymorphic type checking
   • Literature:  https://dl.acm.org/citation.cfm?id=3062357 (PLDI 2017)
   • Supervisor: Christina Jansen
   • Student: Philipp Schröer
10. String Analysis for Vulnerability Detection
    • Literature: https://link.springer.com/chapter/10.1007/978-3-319-23404-5_1 (Model Checking SW 2015, Tutorial PLDI 2016)
    • Supervisor: Christina Jansen
    • Student: Julian Büning
11. Static Detection of DoS Vulnerabilities
    • Literature:  https://link.springer.com/chapter/10.1007/978-3-662-54580-5_1 (TACAS 2017)
    • Supervisor: Christina Jansen
    • Student: Jeremias Lemm
12. Partial Redundancy Elimination
    • Literature: https://pdfs.semanticscholar.org/1951/2e4fccc3fb1bdfc6d1bd00f0aefd1e3c513e.pdf
    • Supervisor: Thomas Noll
    • Student: Hakan Siktas
13. Analyzing undefined behavior of C programs
    • Literature:  http://dl.acm.org/citation.cfm?id=2737979 (PLDI 2015)
    • Supervisor: Tim Lange
    • Student: Justus Fesefeldt

Verification

14. Verification of information-flow security
    • Literature:  http://dl.acm.org/citation.cfm?id=2908100 (PLDI 2016)
    • Supervisor: Thomas Noll
    • Student: Vincent Drury
15. Cartesian Hoare logic for verifying k-safety properties
    • Literature:  http://dl.acm.org/citation.cfm?id=2908092 (PLDI 2016)
    • Supervisor: Tim Lange
    • Student: Sonja Skiba
16. Model checking concurrent programs
    • Literature:  http://dl.acm.org/citation.cfm?id=2737975 (PLDI 2015)
    • Supervisor: –
    • Student: –
17. Verifying pointer programs using separation logic
    • Literature:  http://dl.acm.org/citation.cfm?id=2535871 (POPL 2014)
    • Supervisor: –
    • Student: –

Schedule of Talks

Tuesday 30.01.2018
09:00-10:30	15, 1, 2
10:45-12:15	3, 6, 7
14:00-15:30	4, 5, 13
15:45-16:45	12, 14
Wednesday 31.01.2018
14:00-15:00	8, 9
15:15-16:15	10, 11

Additional Material

• Introductory slides
• Report template
• Presentation template
• How to write scientific papers
• How to give presentations
• Introduction to LaTeX

Registration

Registration to the seminar is handled between Juni 30 and July 16, 2017, via the central online form.

Contact

Thomas Noll <noll at cs.rwth-aachen.de>