Trainings and Tutorials
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 and Dr. Tim Coopman
System Verification Lab (SVL) – Leiden University
Leiden, 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.
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).
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:
Formal methods of program construction were conceived for explaining programming principles to novice programmers. 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 language-independent visualization of correctness theory. 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 suitable for students starting with formal methods or interested in strengthening their programming and for instructors looking to teach a more rigorous approach to programming. The material was used in required courses at McMaster that are not labelled as formal methods courses. The material will be available as an open educational resource and includes a collection of exercises that cover both theory and programming.
Short Bio
Emil Sekerinski is a Professor at McMaster University, Canada. Prior, he had positions at Åbo Akademi, Finland, and Forschungszentrum Informatik, Germany and visiting positions at TU Dresden, Germany, ETH Zürich, Switzerland, and TU Munich, Germany. He studied Computer Science in Stuttgart and Karlsruhe, Germany, and received his Ph.D. from the Karlsruhe Institute of Technology. His interests include programming logic (verification, refinement), concurrency (components, implementation), embedded systems (modelling, analysis), and programming languages (run-time, compilation).
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.