Trainings and Tutorials
An introduction to Runtime Verification
Prof. Dr. Martin Leucker
Institute of Software Engineering and Programming Languages
University of Lübeck, Germany
Abstract:
In this tutorial, we provide an introduction to the field of Runtime Verification, with a particular focus on Linear Temporal Logic (LTL)-based monitor synthesis approaches. We offer a thorough and structured overview of both rewriting and automata-based techniques. Key concepts such as monitors, impartiality, and anticipation are explained within the framework of LTL. Additionally, we include a brief introduction to stream-based runtime verification to further enrich the discussion.
Short Bio
Martin Leucker is currently a professor at the University of Lübeck, Germany heading the Institute of Software Engineering and Programming Languages. He obtained his Ph. D. at the RWTH Aachen, Germany and afterwards, he worked as a Postdoc at the University of Philadelphia, USA and at the Uppsala University, Sweden. He pursued his habilitation at the TU München, Germany. He is the author of more than 130 peer reviewed conference and journal papers ranging over software engineering, formal methods and theoretical computer science.
Abstract and Concrete Model Checking: Through the Lens of Lattice Theory and Category Theory
Prof. Dr. Ichiro Hasuo
Director of Research Center for Mathematical Trust in Software and Systems
National Institute of Informatics – Tokyo, Japan
Abstract:
I will sketch a few aspects of lattice theory and category theory that arise in model checking, demonstrating how they are relevant to some recent techniques such as probabilistic verification by value iteration and compositional model checking. This will serve both as an introduction to model checking and one to abstract studies of mathematical structures.
Short Bio
Ichiro Hasuo, Ph.D., is a Professor at National Institute of Informatics (NII), Tokyo, Japan. He is at the same time the Research Director of the JST ERATO “Metamathematics for Systems Design” Project, and the Director of Research Center for Mathematical Trust in Software and Systems at NII. He received PhD (cum laude) in Computer Science from Radboud University Nijmegen, the Netherlands, in 2008. His research field is software science and his interests include formal verification, mathematical and logical structures, integration of formal methods and testing, and application to cyber-physical systems and systems with statistical machine learning components.
Quantum Circuit Compilation using Formal Methods
Dr. Alfons Laarman
System Verification Lab (SVL)
Leiden University, Netherlands
Dr. Tim Coopmans
QuTech and Delft University of Technology
Netherlands
Abstract:
This tutorial gives an introduction to quantum computing with a focus on the applicability of Formal Methods to Quantum Computing. We will show why formal methods are needed for quantum computing. In particular, we will show how SAT solving and decision diagrams can be used for quantum computing.
This tutorial is aimed for everyone in the formal methods community with an interest in quantum computing. It does not require any prior knowledge on quantum computing. The goal of the tutorial is to get people from the formal methods community inspired by quantum computing.
Short Bio
Alfons Laarman is associate professor at Leiden University, where he leads the System Verification Lab (SVL) and is co-founder of the inter-departmental Applied Quantum Algorithms (aQa) initiative. Prior to moving to Leiden, he was postdoc at the TU Vienna and completed his PhD at University of Twente with distinction (cum laude).
Laarman is known for parallel DFS-based graph algorithms, divide & quantum algorithms, a knowledge compilation map for quantum information and #SAT-based quantum circuit compilation methods. In general, his research spans reliable computing, parallel computing and quantum computing, often bridging theory and practice. His research is funded by several national and European consortia as well as by personal grants from the Dutch Scientific Research Council.
Tim Coopmans is an assistant professor at QuTech and Delft University of Technology. He builds algorithms and software for designing quantum technologies which suffer from hardware imperfections and other errors. He learned about formal methods during a postdoc at Leiden University with Alfons Laarman, and before that completed a PhD at QuTech with David Elkouss and Stephanie Wehner on predicting and optimising real-world performance of networks of quantum computers.
SAT Solvers: Modern Approaches and Applications
Dr. Priyanka Golia
Computer Science and Engineering Department
Indian Institute of Technology Delhi – New Delhi, India
Abstract:
In this lecture, we will delve into the fascinating world of SAT solvers. SAT, or Boolean satisfiability, is a fundamental problem in computer science. At its core, the problem of Boolean satisfiability asks a simple question: given a Boolean formula, can we find an assignment of truth values to its variables that satisfies the formula? Boolean satisfiability is known to be NP-complete. However, modern SAT solvers offer efficient solutions capable of handling problems with tens of thousands of variables and millions of clauses in practical scenarios.
The beauty of SAT solvers lies in their efficiency. They employ sophisticated algorithms and techniques to efficiently explore the vast space of possible variable assignments, searching for a satisfying assignment. In this lecture, we will discover the secret behind modern SAT solvers, moreover, we will also explore how SAT solvers are used in real life, from explainable or certified AI to the verification and synthesis of automated systems, and to optimization problems related to graphs.
Short Bio
Priyanka Golia is an Assistant Professor in the Computer Science and Engineering Department at the Indian Institute of Technology Delhi. Prior to that, she was a faculty at the CISPA Helmholtz Center for Information Security, Germany. She completed her Ph.D. through a joint degree program between Indian Institute of Technology Kanpur, India, and National University of Singapore.
Her research interests lie at the intersection of formal methods and artificial intelligence. Specifically, her work has focused on designing scalable automated synthesis and testing techniques. Her research has received a Best Paper Nomination at ICCAD-21, a Best Paper Candidate at DATE-23, and an invitation for special issues in FMSD. She was named one of the EECS Rising Stars in 2022.
Formal Aspects of Model-Driven Development — A Unified Method
Prof. Dr. Zhiming Liu
Centre for Research and Innovation in Software Engineering (RISE)
Southwest University, Chongqing
Abstract:
Model-driven engineering (MDE), or model-driven architecture (MDA), is attractive to the software industry because it is seen as promising in aiding to master the great and inherent complexity of software through automatic model construction and transformation. Software development companies and organizations are eagerly seeking integrated development platforms (IDP) to greatly improve automation in their software development. However, literature and industry surveys show that the industry adoption of MDE is limited, and there are few success stories about the development and use of IDPs.
In this tutorial, we use the formal refinement of component and object systems (rCOS) as a framework to propose an institution of formal theories, techniques, and tools that are needed in MDE. This implies the need for defining families of languages and transformations, and for developing and linking techniques and tools for these languages. We also argue that architecture modeling and refinement are essential for MDE, and software automation in MDE is crucial to automate model construction, refinement, validation, verification, and integration. To design, implement, and use the automation, multi-dimensional separation of concerns through abstraction, refinement, and decomposition is crucially important, and this is the greatest challenge for software automation. We also outline the challenges in MDE for the emerging human-cyber-physical systems (HCPS).
Short Bio
Zhiming LIU has been working in the area of software theory and methods. He is known for his work on Transformational Approach to Fault-Tolerant and Real-Time Systems, Probabilistic Duration Calculus for System Dependability Analysis,Theory of semantics and refinement of object-oriented programming, rCOS Method for Component-Based Systems. His current research focus is in modelling, design and evolution of human-cyber-physical system (HCPS). Zhiming Liu studied mathematics in university. He holds a MSc in Computing Science from Software Institute of CAS (1988) and a PhD in Computer Science from University of Warwick (1991). Zhiming Liu joined Southwest University in Chongqing as a full-time professor of computer science in 2016. He is leading the development of the University Centre for Research and Innovation in Software Engineering (RISE). Before Southwest University, he worked in three universities in the UK (1988-2005 and 2013-2015) and the United Nations University – International Institute for Software Technology (Macau, 2002-2013).
A Formal Look at Programming
Prof. Dr. Emil Sekerinski
Department of Computing and Software
McMaster University
Abstract:
This training lecture provides an introduction to the classical theory of program correctness. Sequential programming, modularization (object-oriented programming), robustness (exceptions), and concurrency (semaphores, message passing) are covered. The exposition uses a visual formalism to be programming language independent. The algebraic structure of programs is explored. In Interactive Jupyter notebooks, the connection between the theory and common programming languages (e.g. Python, Java, Go, C) is illustrated. The lecture is targeted at students starting with formal methods or interested in strengthening their programming, and at instructors looking to teach a more rigorous approach to programming. The material is available as an open educational resource and has a collection of exercises that cover both theory and programming. The lecture material is accessible.
Short Bio
Emil Sekerinski is a distinguished computer scientist and professor known for his contributions to the fields of formal methods, software engineering, and embedded systems. Currently he is serving as a professor at McMaster University in Canada. Prior to to Canada, he was Associate Professor at Abo AKademi in Turku, Finland. Sekerinsky got is doctoral degree in 1994 at Karlsruhe University, Germany.
Throughout his career, Sekerinski has been instrumental in advancing the understanding and application of formal specification and verification techniques in software development. His research focuses on the design and analysis of dependable software systems, particularly in the context of safety-critical and embedded systems.
ProofBuddy: A Gentle Online Proof Assistant for Learners
Technische Universität Berlin
Berlin, Germany
Abstract:
he use of proof assistants for the development of proofs is similar to the use of an IDE for the development of programs. We introduce the web application ProofBuddy for the proof assistant Isabelle. It is designed as a learning platform for proof development. As such, it serves as a tool to (1) help students to write (mathematical) proofs in a structured way and (2) provide immediate feedback on completeness and correctness. Technically, the web application mediates between web users working on learning tutorials and the proof assistant Isabelle running behind a web server.
We give an overview of the didactic ideas and technical background of our endeavor. Additionally, we explain the user interface, including the (restricted) syntax, and the potential for individualized learning paths. Our tutorial includes hands-on exercises to experience both the student and teacher perspective. Participants should have a background in formal methods.
Short Bios
Uwe Nestmann is professor for models and theory of distributed systems at TU Berlin. His scientific interest spans from purely basic research on models of concurrent and distributed computation to the rigorous analysis of applications using domain-specific model variants and extensions. It is this quest for rigor that drove his interest for the use of proof assistants in research and teaching. He received a Test-of-Time award of the CONCUR conference series in 2021 for his contributions to the understanding of the expressive power of concurrent languages. He holds a doctoral degree from the Universität Erlangen-Nürnberg in Germany and spent almost ten years in France (INRIA), Denmark (BRICS Aalborg), and Switzerland (EPFL).
Nadine Karsten is a PhD student in the research group on models and theory of distributed systems at TU Berlin. Her scientific interest spans from models of distributed computation to the use of proof assistants in undergraduate teaching. Her PhD project addresses the latter domain, especially the question in how far the possibility of instant feedback for proof learners – when using a tool like ProofBuddy – leads to measurably better results in comparison to traditional pen-and-paper ways to teach proof competence.
Venue
The ICTAC 2023 tutorials and training lectures will be held at the campus of the Asian Institute of Technology, Pathum Thani, north of Bangkok on the 25th and 26th of November 2024.
The tutorials target participants who have formal methods background, while the training lectures targets master students, Ph.D. students, early-stage researchers, and lecturers in the field of computer science and mathematics that are not familiar with formal methods and want to get a taste of what formal methods is. Here by formal methods, we intend mathematical approaches to software and system development which support the rigorous specification, design and verification of computer systems.