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).
A Formal Look at Programming
McMaster University
Hamilton, Canada
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).
Probabilistic Datatypes
Computer Science Department, Macquarie University
Sydney, Australia
Abstract:
Datatypes — in which data is encapsulated together with methods that access it — play an important role in the organisation of large software projects. Correctness of datatypes has traditionally been carried out using simulation relations to simplify the verification by separating concerns: the datatype can be verified independently from the programs that use it, whilst those programs themselves can be verified using the specifications of the datatype’s methods.
In this talk I introduce the idea of probabilistic datatypes in which probabilistic choices are used to implement probabilistic specifications. I will show, by example, how the standard Markov Decision Process model fails the well known “copy rule” when both nondeterminism and probability are present, and that a more sophisticated model using ideas from the theory of Quantitative Information Flow is necessary for sound proof rules based on the well-known technique of simulations.
Short Bio
Annabelle McIver is a professor of Computer Science at Macquarie University in Sydney, and co-director of the Future Communications Research Centre. Annabelle trained as a mathematician at Cambridge and Oxford Universities. Her research uses mathematics to prove quantitative properties of programs, and more recently to provide foundations for quantitative information flow for analysing security properties. She is co-author of the book “Abstraction, Refinement and Proof for Probabilistic Systems”, and “The Science of Quantitative Information Flow”.
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.