Prof.Martin Georg Fränzle

M. Fränzle’s holds the chair of Foundations and Applications of Systems of Cyber-Physical-Systems at the university of Oldenburg in Germany, where he also was dean of the School of Computing Science, Business Administration, Economics, and Law as well as Vice President Research, Transfer and Digitalization of the university. His research interests are in modelling, verification, and synthesis of reactive, real-time, and hybrid dynamics in embedded, cyber-physical, and human-cyber-physical systems. His work spans the semantic foundations of high-level modeling and specification languages as well as decision problems and their application to verifying and synthesizing real-time and hybrid discrete-continuous systems, including settings subject to stochastic disturbances.

His contributions to the extension of SAT-modulo-theory solving to the undecidable domains of arithmetic constraints involving transcendental functions have generated one of the very few commercially successful automatic verification tools for hybrid-state systems (iSAT, under distribution by BTC ES AG).Fränzle has co-authored more than 190 articles primarily in computer science, but also in communication engineering, applied neuroscience, and physics and has edited several special issues of journals as well as proceedings volumes. He has been member of the board of the Transregional Collaborative Research Center SFB-TR 14 AVACS, as well as of the Research Training Groups DFG GRK 1765 SCARE, DFG GRK 1076 TrustSoft, SAMS (Safe Automation of Maritime Systems), and SEAS (Social Embeddedness of Autonomous Cyber Physical Systems) at the university of Oldenburg. His research received funding from DFG, BMBF, BMWI, the State of Lower Saxony, VDA, Velux Fonden, and the EU, as well as through direct industrial research contracts with Volkswagen, Daimler, DENSO Automotive, and BTC ES AG.

This lecture is split into two parts:

1. We will go over the construction of a digital twin exemplified by an incubator system, including the benefits and challenges of each application. The result is a description of the building blocks of a digital twin as well as an example of self-adaptation.

2. We discuss formal verification of self-adaptations, and their role in avoiding the re-certification of reconfigured CPS. In addition, we demonstrate constructing a non-deterministic model which captures the uncertainties in the system behaviour after a self-adaptation. We use Signal Temporal Logic to specify the safety requirements the system must satisfy after reconfiguration and employ formal methods based on verified monitoring over Flow* flowpipes to check these properties at runtime. This gives us a framework to predictively detect and mitigate unsafe self-adaptations before they can lead to unsafe states in the physical system.

Title 2: Building and Deploying a Digital Twin Service

Prof. Cláudio Gomes

Prof. Cláudio Gomes is an Associate Professor of Software Engineering & Computing systems in the Department of Electrical and Computer Engineering at Aarhus University. His research focuses on the co-simulation and the engineering of digital twins – including Simulation, Digital Twin, Models, Cyber Physical Systems, Algorithms, Semantics, Standards, Interface Standards, and so on. He is the author and co-author of over 80 papers and received the Runner Up Best Paper Award at ANNSIM Conference (in 2023). He is the guest editor for the SIMULATION journal and the reviewer for 8 different journals in the past 2 years.

Prof. Zhiming Liu

Zhiming Liu is a professor at Southwest University, Chongqing, China. His research interests lie in the area of software theory and methods, with a particular focus on the modeling, design, and verification of software and systems. He is renowned for his work on the Transformational Approach to Fault-Tolerant and Real-Time Systems, Probabilistic Duration Calculus for System Dependability Analysis, the theory of semantics and refinement of object-oriented programming, and the rCOS method for component and object system modeling and refinement. Zhiming Liu’s recent research revolves around the computational model, models, and refinement of software systems for human-cyber-physical systems (HCPS) and trustworthy autonomous systems (TAS). Together with his colleagues, he has recently proposed a model of human-cyberphysical automata (HCPA) for HCPS to characterize interactions, concurrency, and coordination behavior of human agents, intelligent machine agents, and physical objects and processes.

Zhiming Liu studied mathematics at university and holds an MSc in Computing Science from the Software Institute of CAS (1988) and a PhD in Computer Science from the University of Warwick (1991). Before joining Southwest University in Chongqing as a full-time professor in 2016, he worked at the University of Leicester as a lecturer (1994-2005), at the United Nations University - International Institute for Software Technology as a research fellow and then a senior research fellow (UNU-IIST, Macao, 2002-2013), and at Birmingham City University as the Chair Professor of Engineering (2013-2015).

Prof. Kuldeep Meel

Kuldeep Meel is an Associate Professor of Computer Science in the Department of Computer Science at the University of Toronto. His research interests lie at the intersection of Formal Methods and Artificial Intelligence. He is a recipient of the 2022 ACP Early Career Researcher Award, the 2019 NRF Fellowship for AI, and was named AI's 10 to Watch by IEEE Intelligent Systems in 2020. His research program's recent recognitions include the 2023 CACM Research Highlight Award, 2022 ACM SIGMOD Research Highlight, IJCAI-22 Early Career Spotlight, Distinguished Paper Award at CAV-23, "Best Papers of CAV" (2020 and 2022) special issue in FMSD journal, Best Paper Award nominations at ICCAD-21 and DATE-23, 1st Place in Model Counting Competition (2020 and 2022). He is passionate about teaching, and most proud of being recipient of university-level Annual Teaching Excellence Awards in 2022 and 2023.

Before moving to Toronto in 2023, he held NUS Presidential Young Professorship in the School of Computing at the National University of Singapore. Before joining NUS in Spring 2018, he received M.S. and Ph.D. from Rice University, co-advised by Supratik Chakraborty and Moshe Y. Vardi. His thesis work received the 2018 Ralph Budd Award for Best Ph.D. Thesis in Engineering and the 2014 Outstanding Masters Thesis Award from Vienna Center of Logic and Algorithms, IBM Ph.D. Fellowship, and Best Student Paper Award at CP 2015. He graduated with Bachelor of Technology (with honors) in Computer Science and Engineering from IIT Bombay.

Title :Debugging, Verification and Repair of Deep Neural Networks

Abstract : Artificial intelligence (AI), especially deep neural networks (DNNs), has been widely used, in the meanwhile posing significant safety and security concerns. In this course, we address these challenges by exploring the use of software engineering approach and formal verification method for diagnosing and fixing defects in DNNs. In addition to theoretical concepts, this course will include a practical session of installing and running the software tools. Participants are encouraged to download and install the tools and follow the step-by-step instructions during the session.

Prof. Jean-Pierre Talpin

Jean-Pierre Talpin is a senior scientist (directeur de recherche) with INRIA. He received a Master degree in Theoretical Computer Science from University Paris VI and did his Ph.D. Thesis with Ecole des Mines de Paris under the supervision of Pierre Jouvelot. He then joined the European Computer-Industry Research Centre in Munich for three years before being hired by INRIA in 1995, where he led Inria project-teams ESPRESSO and TEA from 2000 to 2023.Among his 150 co-authored articles, Jean-Pierre Talpin received the 2004 ACM Award for the most influential POPL paper (for 1994) with Mads Tofte and the 2012 ACM/IEEE LICS Test of Time Award (for 1992) with Pierre Jouvelot, both for his early-carrier works on region-based memory management.

From his career-long studies in logic, type, concurrency theory and his experiences in program analysis and verification, avionics and cybernetic system design, his research interests have lately focused on novel and challenging topics such as end-to-end mechanized program verification, the design of advanced process calculi to model the logic of mobile, dynamic cyber-physical system networks and of compositional algebraic methodologies to verify them.

Title : Machine Learning and Logic: Fast and Slow Thinking (Online)

Abstract : Computer science seems to be undergoing a paradigm shift. Much of earlier research was conducted in the framework of well-understood formal models. In contrast, some of the hottest trends today shun formal models and rely on massive data sets and machine learning.A cannonical example of this change is the shift in AI from logic programming to deep learning. I will argue that the correct metaphore for this development is not paradigm shift, but paradigm expansion. Just as General Relativity augments Newtonian Mechanics, rather than replace it -- we went to the moon, after all, using Newtonian Mechanics — data-driven computing augments model-driven computing. In the context of Artificial Intelligence, machine learning and logic correspond to the two modes of human thinking: fast thinking and slow thinking.The challenge today is to integrate the model-driven and data-driven paradigms. I will describe one approach to such an integration -- making logic more quantitative.

Prof. Moshe Y. Vardi

Moshe Y. Vardi is University Professor and the George Distinguished Service Professor in Computational Engineering at Rice University. His research focues on the interface of mathematical logic and computation -- inluding database theory, hardware/software dessign and verification, multi-agent systems, and constraint satisfaction. He is the recipient of numerous awards, including the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Knuth Prize, the IEEE Computer Society Goode Award, and the EATCS Distinguished Achievements Award. He is the author and co-author of over 750 papers, as well as two books. He is a Guggenheim Fellows as well as fellow of several societies, and a member of several academies, including the US National Academy of Engineering, National Academy of Science, and the Royal Society of London. He holds nine honorary titles. He is a Senior Editor of the Communications of the ACM, the premier publication in computing.