Invited Talks

Erika Abraham graduated at the Christian-Albrechts-University Kiel (Germany), and received her PhD from the University of Leiden (The Netherlands) for her work on the development and application of deductive proof systems for concurrent programs. Then she moved to the Albert-Ludwigs-University Freiburg (Germany), where she started to work on the development and application of SAT and SMT solvers. Since 2008 she is professor at RWTH Aachen University (Germany), with main research focus on SMT solving for real and integer arithmetic, and formal methods for probabilistic and hybrid systems.

Title: SMT Solving: Past, Present and Future

Abstract: Since the development of the first computer algebra systems in the '60s, automated decision procedures for checking the satisfiability of logical formulas gained more and more importance. Besides symbolic computation techniques, some major achievements were made in the '90s in the relatively young area of satisfiability checking, and resulted in powerful SAT and SAT-modulo-theories (SMT) solvers. Nowadays, these sophisticated tools are at the heart of many techniques for the analysis of programs and probabilistic, timed, hybrid and cyber-physical systems, for test-case generation, for solving large combinatorial problems and complex scheduling tasks, for product design optimisation, planning and controller synthesis, just to mention a few well-known areas. In this talk we give a historical overview of this development, describe our own solver SMT-RAT and discuss some fascinating new developments for checking the satisfiability of real-arithmetic formulas.

Saddek Bensalem (University Grenoble Alpes, VERIMAG, Grenoble, France)

Title: Rigorous System Design for AI Software

Klaus-Dieter Schewe received his Ph.D. in Mathematics from the University of Bonn in 1985 and his D.Sc. in Theoretical Computer Science from the Brandenburgian Technical University in 1995. He held positions in industry, at the Universities of Hamburg, Cottbus, Clausthal-Zellerfeld, Linz and at Massey University, and he worked as CSO of the Software Competence Center Hagenberg. Since 2019 he is full professor at Zhejiang University at its international Campus in Haining. His main research interests are in rigorous methods, theoretical computer science, logic and database theory.

Title: Practical Theory of Computation on Structures

Abstract: There are hardly two fields in Computer Science that are further apart than Software Engineering and Theoretical Computer Science. The lack of theoretical foundations in the field of Software Engineering, which is alien to other engineering disciplines, has a counterpart in a lack of interest in practical usability of computation theory. Nowadays we are dealing with complex systems of systems, but it seems that the theoretical foundations have not caught up with the development. This raises the question how a theory of computation should look like that modernises the classical theory and at the same time is suitable for practical systems development. This presentation is dedicated to a sketch of such a theory of computation centred around the notion of algorithmic systems, which are harder to define than computable functions, in particular, when all developments in computing are to be taken into account. I will argue that behavioural theories are key to the understanding, i.e. we require language-independent axiomatic definitions of classes of algorithmic systems that are accompanied by abstract machine models provably capturing the class under consideration. The machine models give further rise to tailored logics through which properties of systems in the considered class can be formalised and verified, and to fine-tuned classifications on the grounds of complexity restrictions. I will outline that all extensions will be (1) conservative in the sense that the classical theory of computation is preserved, (2) universal in the sense that all practical developments are captured uniformly, and (3) practical in the sense that languages associated with the abstract machine models can be used for rigorous high-level systems design and development, and the logics can be exploited for rigorous verification of desirable properties of systems.

SUN, Jun is currently a professor at Singapore Management University (SMU). He received Bachelor and PhD degrees in computing science from National University of Singapore (NUS) in 2002 and 2006. He has been a faculty member since 2010. Jun's research interests include formal methods, software engineering, and cyber-security. He is the co-founder of the PAT model checker. He has published more than 200 articles and conference papers including top conferences in multiple areas.

Title: Neural Network Fairness: Verification and Repair

Abstract: Fairness is crucial for neural network applications with important societal implications (such as personal credit rating). In this talk, I will present our recent research on neural network discrimination, from the perspective of evaluation, mitigation, and certification. In particular, we propose an approach to formally verify neural networks against fairness. Our method is built upon an approach for learning Markov Chains from a user-provided neural network which is guaranteed to facilitate sound analysis of global properties. We further show that through causality analysis, we can systematically identify the cause of discrimination and repair the neural network effectively and efficiently.