Seminar in Theoretical CS, Summer Semester 2018

News

• 19.01.2018: we are online

Deadlines

April 12	Kick-off meeting at seminar room of i2 (building E1, room 4201b); here are the presentation slides
May 14	Detailed outline of report due
June 11	Full report due
July 2	Presentation slides due
July 19	Seminar talks (see below for schedule)

Overview

The term formal verification refers to theory and practice of computer-supported mathematical analysis methods for ensuring correctness of software (and hardware) systems. The modeling and verification of such systems is an important issue. In particular, safety-critical systems are ones in which errors can be disastrous: loss of life, major financial losses, etc. Techniques to safeguard against such scenarios are essential for such systems. Testing can identify problems, especially if done in a rigorous fashion, but is generally not sufficient to guarantee a satisfactory level of quality. The latter (additionally) requires proving correctness of systems via automated deduction, e.g., using theorem proving or model checking as a core reasoning method.

A prominent field related to artificial intelligence (AI) is the one of machine learning (ML). Very broadly, machine learning describes algorithms that independently learn from data that is observed in possibly unknown environments. Applications are – only to mention a few – given in autonomous systems, computer vision, and video games. In the real world, these previously not well-defined environments carry the risk of taking safety-critical action along the way of obtaining optimal strategies.

Growing application areas for machine learning, such as autonomous driving, require the exclusion or likely avoidance of unsafe behaviors. An important question is then, how confidence in system behaviors obtained from machine learning can be transferred to formal verification. Vice versa, industrial usage of verification methods such as model checking still suffers from scalability issues for large applications. Leveraging the capabilities of machine learning to assess large data sets will help to enable the verification for more realistic systems. The following directions are particularly important:

• Safety-related issues for machine learning
• Explainability in AI and in model checking
• Scalability and applicability of formal verification

Prerequisites

Basic knowledge in the following areas is expected:

• Formal languages and automata theory
• Mathematical logic

Previous knowledge in either of the two fields of formal verification and machine learning is helpful but not mandatory.

Schedule of Talks

Morning session at i1 seminar room [building E1, ground floor]
09:00-10:30	1, 11, 5
10:45-12:15	6, 10
Afternoon session at i2 seminar room [building E1, room 4201b]
14:00-15:30	4, 12, 14
15:45-16:45	16, 18

Topics

Verification of Properties

1. Safety Verification of Deep Neural Networks
   • Literature: Xiaowei Huang, Marta Kwiatkowska, Sen Wang, Min Wu:
     Safety Verification of Deep Neural Networks. CAV 2017
   • Supervisor: Matthias Volk
   • Student: Valeriia Volkovaia
2. Verification of Markov Decision Processes Using Learning Algorithms
   • Literature: Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma: Verification of Markov Decision Processes Using Learning Algorithms. ATVA 2014
   • Supervisor: –
   • Student: –
3. Smoothed Model Checking
   • Literature: Luca Bortolussi, Dimitrios Milios, Guido Sanguinetti: Smoothed model checking for uncertain Continuous-Time Markov Chains. Inf. Comput. 247: 235-253 (2016)
   • Supervisor: –
   • Student: –
4. Formal Verification of Neural Networks
   • Literature: Rüdiger Ehlers: Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks. ATVA 2017
   • Supervisor: Tim Quatmann
   • Student: Erik Van Loo
5. Verification and Control of Partially Observable Probabilistic Systems
   • Literature: Gethin Norman, David Parker, Xueyi Zou: Verification and control of partially observable probabilistic systems. Real Time Systems, 2017
   • Supervisor: Sebastian Junges
   • Student: Hua Mengzhe
6. Counterexample Explanation for Probabilistic Systems
   • Literature: Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Andreas
     Fellner, Jan Kretínský: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. CAV 2015
   • Supervisor: Tim Quatmann
   • Student: Torben Friedrichs

Learning of Invariants

7. Learning Software Invariants
   • Literature: Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider: ICE: A Robust Framework for Learning Invariants. CAV 2014
   • Supervisor: –
   • Student: –
8. Learning Data Structure Invariants
   • Literature: Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider: Learning Universally Quantified Invariants of Linear Data Structures.
     CAV 2013
   • Supervisor: –
   • Student: –
9. Syntax-Guided Invariant Synthesis
   • Literature: Grigory Fedyukovich and Rastislav Bodik. Accelerating Syntax-Guided Invariant Synthesis. TACAS 2018
   • Supervisor: –
   • Student: –
10. Synthesizing Inductive Invariants
    • Literature: Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik: IC3 – Flipping the E in ICE. VMCAI 2017
    • Supervisor: Benjamin Kaminski
    • Student: Isabelle Tülleners

Model Learning

11. Generating Models of Communication Protocols
    • Literature: 
      • Frits W. Vaandrager: Model learning. Commun. ACM 60(2): 86-95 (2017)
      • Fides Aarts, Bengt Jonsson, Johan Uijen, Frits W. Vaandrager: Generating models of infinite-state communication protocols using regular inference with abstraction. Formal Methods in System Design 46(1): 1-41 (2015)
    • Supervisor: Sebastian Junges
    • Student: Niklas Macherey
12. Learning Finite Automata
    • Literature: Benedikt Bollig, Peter Habermehl, Carsten Kern, Martin Leucker: Angluin-Style Learning of NFA. IJCAI 2009
    • Supervisor: Philipp Berger
    • Student: Robin Drahovsky
13. Learning and Planning with Timing Information in Markov Decision Processes
    • Literature: Pierre-Luc Bacon, Borja Balle, Doina Precup: Learning and Planning with Timing Information in Markov Decision Processes. UAI 2015
    • Supervisor: –
    • Student: –

Synthesis of Programs and Algorithms

14. Policy Learning in Continuous-Time Markov Decision Processes
    • Literature: Ezio Bartocci, Luca Bortolussi, Tomás Brázdil, Dimitrios Milios, Guido Sanguinetti: Policy learning in continuous-time Markov decision processes using Gaussian Processes. Perform. Eval. 116: 84-100 (2017)
    • Supervisor: Thomas Noll
    • Student: Suchanda Bhattahcaryya
15. Safety-Constrained Reinforcement Learning for Markov Decision Processes
    • Literature: Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen: Safety-Constrained Reinforcement Learning for MDPs. TACAS 2016
    • Supervisor: –
    • Student: –
16. Learning Static Analyzers
    • Literature: Pavol Bielik, Veselin Raychev, Martin T. Vechev: Learning a Static Analyzer from Data. CAV 2017
    • Supervisor: Christoph Matheja
    • Student: Tobias Johnen
17. Learning Disjunctions of Predicates
    • Literature: Nader H. Bshouty, Dana Drachsler-Cohen, Martin T. Vechev, Eran Yahav: Learning Disjunctions of Predicates. COLT 2017
    • Supervisor: –
    • Student: –
18. Learning Explanatory Rules from Noisy Data
    • Literature: Richard Evans, Edward Grefenstette: Learning Explanatory Rules from Noisy Data. To appear in Journal of Artificial Intelligence Research
    • Supervisor: Thomas Noll
    • Student: Jan Philipp Hafer
19. Discovery of Divide-&-Conquer Algorithms
    • Literature: Rezaul Chowdhury, Pramod Ganapathi, Stephen L. Tschudi, Jesmin Jahan Tithi, Charles Bachmeier, Charles E. Leiserson, Armando Solar-Lezama, Bradley C. Kuszmaul, Yuan Tang: Autogen: Automatic Discovery of Efficient Recursive Divide-&-Conquer Algorithms for Solving Dynamic Programming Problems. TOPC 4(1): 4:1-4:30 (2017)
    • Supervisor: –
    • Student: –
20. Learning by Program Synthesis
    • Literature: Kevin Ellis, Armando Solar-Lezama, Joshua B. Tenenbaum: Unsupervised Learning by Program Synthesis. NIPS 2015
    • Supervisor: –
    • Student: –
21. Multi-Objective Policy Generation for Mobile Robots
    • Literature: Bruno Lacerda, David Parker, Nick Hawes: Multi-Objective Policy Generation for Mobile Robots under Probabilistic Time-Bounded Guarantees. ICAPS 2017
    • Supervisor: –
    • Student: –

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 January 19 and February 2, 2018, via the central online form.

Contact

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