Seminar in Theoretical CS, Winter Semester 2015/16

News

• 05.11.2015: Topics assigned
• 22.06.2015: we are online

Deadlines

Overview

The goal of this seminar is to give an overview of the related research activities of the MOVES group. It covers several areas of computer science to which computed-aided verification techniques are central, and which represent the research fields of the respective supervisors. Each area features a number of topics which are described in a scientific journal or conference article. These research articles are the basis on which students have to prepare their report and presentation.

The following list gives an overview of the areas that will be covered. For getting an overview of possible related topics, we refer to the previous seminar in winter semester 2014/15.

• Abstraction methods for pointer programs
• Verification methods for Programmable Logic Controller (PLC) software
• Semantics and verification of probabilistic systems
• Formal methods for security analysis

Topics

Inductive Verification

1. Efficient Abstraction Refinement
   • Literature:
     • Johannes Birgmeier, Aaron R. Bradley, Georg Weissenbacher: Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)
   • Supervisor: Tim Lange
   • Student: Nico Wübbels
2. Efficient Computation of Weakest Preconditions
   • Literature:
     • K. Rustan M. Leino: Efficient Weakest Preconditions
     • David Brumley, Ivan Jager: Efficient Directionless Weakest Preconditions
   • Supervisor: Tim Lange
   • Student: Patricia Wessel
3. Property-Directed Inference
   • Literature: A. Karbyshev, N. Bjørner, S. Itzhaky, N. Rinetzky, S. Shoham: Property-Directed Inference of Universal Invariants or Proving Their Absence
   • Supervisor: Tim Lange
   • Student: Frederick Prinz

Analysis of Dynamic Communication and Data Structures

4. Analysis of infinite-state graph transformation systems
   • Literature:
     • Peter Backes, Jan Reineke: Analysis of infinite-state graph transformation systems by cluster abstraction
   • Supervisor: Christina Jansen
   • Student: Isabelle Tülleners
5. Analysis of heap structures with data
   • Literature:
     • Pietro Ferrara, Peter Müller, Milos Novacek: Automatic Inference of Heap Properties Exploiting Value Domains
   • Supervisor: Christina Jansen
   • Student: Lukas Oßmann
6. Analysis of concurrent data structures
   • Literature:
     • Parosh Aziz Abdulla, Frédéric Haziza, Lukáš Holík, Bengt Jonsson, Ahmed Rezine: An integrated specification and verification technique for highly concurrent data structures
   • Supervisor: Christina Jansen
   • Student: Tristan Döhl

Probabilistic and Approximate Computations

7. Cost-Based Analysis of Probabilistic Programs (English only!)
   • Literature:
     • Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs, O. Celiku and A. McIver, FM 2005
   • Supervisor: Federico Olmedo
   • Student: Ravi Singh
8. Relational Hoare Logic for Probabilistic Programs (English only!)
   • Literature:
     • Probabilistic Relational Reasoning for Differential Privacy, G. Barthe, B. Köpf, F. Olmedo and S. Zanella, POPL 2012
   • Supervisor: Federico Olmedo
     
   • Student: Diwahar Jawahar
9. Correctness of Approximate Computations (English only!)
   • Literature:
     • Proving Acceptability Properties of Relaxed Nondeterministic Approximate Programs, M Carbin, D Kim, S Misailovic and MC Rinard, PLDI 2012
   • Supervisor: Federico Olmedo
   • Student: –

Formal Approaches to Systems Engineering

10. Formal requirements engineering(English only!)
    • Literature:
      • M. Autili, L. Grunske, M. Lumpe, P. Pelliccione, A. Tang. Aligning Qualitative, Real-Time, and Probabilistic Property Specification Patterns Using a Structured English Grammar
    • Supervisor: Harold Bruintjes
    • Student: –
11. Contract-based safety assessment (English only!)
    • Literature:
      • M. Bozzano, A. Cimatti, C. Mattarei, S. Tonetta: Formal Safety Assessment via Contract-Based Design
    • Supervisor: Harold Bruintjes
    • Student: Oleg Chernikov
12. Probabilistic safety and liveness (English only!)
    • Literature:
      • J.-P. Katoen, L. Song and L. Zhang. Probably safe or live
    • Supervisor: Harold Bruintjes
    • Student: Alina Shigabutdinova

Automata, Logics, and Games

13. The Cyclic-Routing Problem (English only!)
    • Literature:
      • Hsi-Ming Ho, Joel Ouaknine: The Cyclic-Routing UAV Problem is PSPACE-Complete
      • Rajeev Alur, David L. Dill: A theory of timed automata
    • Supervisor: Souymodip Chakraborty
    • Student: Umair Muslim
14. Pareto Curves for probabilistic Model Checking (English only!)
    • Literature:
      • Vojtech Forejt, Marta Kwiatkowska, and David Parker: Pareto Curves for probabilistic Model Checking
      • V. Forejt, M. Kwiatkowska, G. Norman, D. Parker and H. Qu.: Quantitative Multi-Objective Verification for Probabilistic Systems.
      • Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M: Multi-objective model checking of Markov decision processes.
    • Supervisor: Souymodip Chakraborty
    • Student: –
15. Finite Optimal Control for Time-Bounded Reachability in CTMDPs and Continuous-Time Markov Games (English only!)
    • Literature:
      • Markus N. Rabe and Sven Schewe: Finite Optimal Control for Time-Bounded Reachability in CTMDPs and Continuous-Time Markov Games
      • Martin R. Neuhäußer Lijun Zhang: Time-Bounded Reachability Probabilities in Continuous-Time Markov Decision Processes
      • Krishnendu Chatterjee, Marcin Jurdziński, Thomas A. Henzinger: Quantitative Stochastic Parity Games
    • Supervisor: Souymodip Chakraborty
    • Student: –

Information Flow Analysis for Security

16. Type-based information flow analysis
    • Literature: S. Hunt, D. Sands: On Flow-Sensitive Security Types
    • Supervisor: Thomas Noll
    • Student: Louis Wachtmeister
17. Information flow analysis based on program dependence graphs
    • Literature: Christian Hammer, Gregor Snelting: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs
    • Supervisor: Thomas Noll
    • Student: Moritz Dederichs
18. Model-driven information flow analysis
    • Literature: Najah Ben Said, Takoua Abdellatif, Saddek Bensalem, Marius Bozga: Model-Driven Information Flow Security for Component-Based Systems
    • Supervisor: Thomas Noll
    • Student: Thomas Mertens

Formal Methods in System Design

19. Model checking and performance of shared-memory mutual exclusion protocols
    • Literature: R. Mateescu and W. Serwe: Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols
    • Supervisor: Hao Wu
    • Student: Raoul Schaffranek
20. Modelling and Analysis of Markov Automata
    • Literature: D. Guck, H. Hatefi, H. Hermanns, J.-P. Katoen, M. Timmer:Analysis of Timed and Long-Run Objectives for Markov Automata
    • Supervisor: Hao Wu
    • Student: Cagatay Ogut
21. Model Checking Linearizability via Refinement
    • Literature: Y. Liu, W. Chen, Y. A. Liu, and J. Su: Model Checking Linearizability via Refinement
    • Supervisor: Hao Wu
    • Student: –

Schedule of Talks

Prerequisites

Basic knowledge in the following areas is expected:

• Formal languages and automata theory
• Mathematical logic
• Previous knowledge in semantics of programming languages and concurrency theory is helpful but not mandatory

Registration

Registration to the seminar is handled between June 25 and July 8, 2015, via the central online form.

Additional Material

Contact

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