Seminar in Theoretical CS, Summer 2021

### News

- 07.12.2020: we are online

### Dates & Deadlines

14.04.2021 15:00 | Introduction (Zoom meeting) |

18.04.2021 | Topic preferences due |

10.05.2021 | Detailed outline due |

07.06.2021 | Seminar report due |

28.06.2021 | Presentation slides due |

13.07.2021 | Seminar |

### Introduction and Assignment of Topics

### Overview

The term *Computer-Aided Verification* refers to theory and practice of computer-supported formal analysis methods for both hardware and software systems. Likewise, it is the name of an annual academic conference on that topic. 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. Formal methods, on the other hand, offer techniques ranging from the description of requirements in a formal notation to allow for rigorous reasoning about them, to techniques for automatic verification of software. Due to the complexity of these approaches and the systems they are applied to, automated computer support is indispensable.

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.

### Schedule of Talks

Time | Tuesday, July 13 |

11:00-12:30 | Philipp Roytburg, Sebastian Kramm, Marvin Vogt |

14:00-15:00 | Yifei Xu, Markus Miliats |

15:15-16:15 | Raufu Miah, Thomas Schneider |

### Topics

(The annotations “B” and “M” respectively refer to topics on Bachelor and Master level.)

#### Robustness Analysis of Neural Networks

- Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, Suman Jana:
*Efficient Formal Safety Analysis of Neural Networks*, NeurIPS 2018 (B/M)- Student: –
- Supervisor: Christopher Brix

- Patrick Henriksen, Alessio Lomuscio:
*Efficient Neural Network Verification via Adaptive Refinement and Adversarial Search*, ECAI 2020 (M)- Student: Philipp Roytburg
- Supervisor: Christopher Brix

- Hoang-Dung Tran, Diago Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang:
*Star-Based Reachability Analysis of Deep Neural Networks*, FM 2019 (M)- Student: –
- Supervisor: Christopher Brix

- Jianlin Li, Jiangchao Liu, Pengfei Yang, Liqian Chen, Xiaowei Huang, Lijun Zhang:
*Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification*, SAS 2019 (B/M)- Student: –
- Supervisor: Thomas Noll

- Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue, Lijun Zhang:
*Improving Neural Network Verification through Spurious Region Guided Refinement*, TACAS 2021 (B/M)- Student: Sebastian Kramm
- Supervisor: Thomas Noll

- Michael Everett, Golnaz Habibi, Jonathan P. How:
*Robustness Analysis of Neural Networks via Efficient Partitioning with Applications in Control Systems*, IEEE CSL 2020 (M)- Student: –
- Supervisor: Thomas Noll

#### Analysis of Bayesian Networks

- Ezio Bartocci, Laura Kovács, Miroslav Stankovic:
*Analysis of Bayesian Networks via Prob-Solvable Loops*. ICTAC 2020: 221-241 (B/M)- Student: Yifei Xu
- Supervisor: Bahare Salmani

- Andy Shih, Arthur Choi, Adnan Darwiche:
*Formal Verification of Bayesian Network Classifiers*. PGM 2018: 427-438 (B/M)- Student: Markus Miliats
- Supervisor: Bahare Salmani

- Arthur Choi, Ruocheng Wang, Adnan Darwiche:
*On the relative expressiveness of Bayesian and neural networks*. Int. J. Approx. Reason. 113: 303-323 (2019) (M)- Student: –
- Supervisor: Bahare Salmani

#### Synthesizing Quantitative Loop Invariants for Probabilistic Programs

- Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia:
*Finding Polynomial Loop Invariants for Probabilistic Programs*. ATVA 2017 (M)- Student: –
- Supervisor: Mingshuai Chen

- Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, Justin Hsu:
*Synthesizing Probabilistic Invariants via Doob’s Decomposition*. CAV 2016 (M)- Student: –
- Supervisor: Mingshuai Chen

- Ezio Bartocci, Laura Kovács, Miroslav Stankovič:
*Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops*. ATVA 2019 (M)- Student: Marvin Vogt
- Supervisor: Mingshuai Chen

#### Formal Approaches to Systems Engineering

- Ola Bäckström, Yuliya Butkova, Holger Hermanns, Jan Krčál, and Pavel Krčál:
*Effective Static and Dynamic Fault Tree Analysis*. SAFECOMP 2016 (B)- Student: Raufu Miah
- Supervisor: Shahid Khan

- Barbara Kordy, Sjouke Mauw, Sasa Radomirovic, and Patrick Schweitzer:
*Attack-Defense Trees*, J. Log. Comput. 24, 2014 (B)- Student: –
- Supervisor: Shahid Khan

- Z. Aslanyan, F. Nielson, and D. Parker:
*Quantitative Verification and Synthesis of Attack-Defence Scenarios.*CSF 2016 (B/M)- Student: Thomas Schneider
- Supervisor: Shahid Khan

### Prerequisites

Basic knowledge in the following areas is expected:

- Formal languages and automata theory
- Mathematical logic
- Probability Theory

Previous knowledge in semantics of programming languages and concurrency theory is helpful but not mandatory

### Registration

Registration to the seminar is handled via the SuPra**.**

### Additional Material

- Report template
- Presentation template
- How to Write a Seminar Paper
- Ethische Richtlinien für das Verfassen wissenschaftlicher Arbeiten
- How to Give Presentations
- Introduction to LaTeX

### Contact

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