Welcome to Summer School on Formal Methods


August 06-August 15, 2019


Courses

Title: Verification and Understanding of Deep Learning (Part 1)
Lecturer: Prof. Xiaowei Huang
Abstract:  
The past few years have seen deep learning achieved human-level intelligence in several tasks, such as image processing and video game playing, and been applied to many application areas, including robotics control, healthcare, etc. While the empirical precision has been significantly improved, deep learning suffers from the problem of lacking certification and understanding... more details

Title: Verification and Understanding of Deep Learning (Part 2)
Lecturer: Prof. Xinping Yi
Abstract:
The past few years have seen deep learning achieved human-level intelligence in several tasks, such as image processing and video game playing, and been applied to many application areas, including robotics control, healthcare, etc. While the empirical precision has been significantly improved, deep learning suffers from the problem of lacking certification and understanding... more details

Title: Requirements formalization and correctness-by-construction
Lecturer: Prof. Panagiotis Katsaros
Abstract:
In the model-driven design of software and systems, approaches aiming to achieve correctness-by-construction are a natural alternative towards avoiding the well-known scalability limitations of model checking. Ensuring correctness by design rather than through verification is the main challenge of a few worthy research efforts during the last few years. We present two different perspectives of correctness-by-construction and the associated design frameworks developed in our recent research work... more details

Title: Foundations of Cyber-Physical Systems
Lecturer: Dr. Stefan Mitsch
Abstract:
Cyber-physical systems (CPS) are today pervasively embedded into our lives and increasingly act in close proximity as well as with direct impact to humans. For example, driver assistance systems in cars are responsible for controlling acceleration and braking on the basis of distance sensors. Further prominent examples can be found in many safety-critical areas where lives are at stake, such as in factory automation, medical equipment, aviation, automotive, railway industries, and robotics. Formal verification techniques are particularly suitable to provide the necessary correctness guarantees at the necessary level of trust... more details

Title: Rewrite based Automated Reasoning Algorithms for System Analysis
Lecturer: Prof. Deepak Kapur
Abstract:
The short course will cover various automated reasoning algorithms the author has used for hardware and software analysis... more details

Title: Speaking Logic
Lecturer: Prof. Natarajan Shankar
Abstract
Formal logic has become the lingua franca of computing. It is used for specifying digital systems, annotating programs with assertions, defining the semantics of programming languages, and proving or refuting claims about software or hardware systems... more details