From topological proofs and beyond.
Watch the video
Download the presentation slides (PDF)
Synopsis
Model checking provides developers with helpful information to improve their models when a property is not satisfied by a counterexample. However, engineers need helpful information also when a property is instead satisfied. This seminar will introduce Topological Proofs: slices of the model that witness the correctness of systems by justifying property satisfaction. It will present TOrPEDO, an approach that supports their use.
It will discuss two complementary versions of this approach: the first based on unsatisfiable cores of LTL formulae and an enhanced and more efficient version that relies on a novel encoding of LTL formulae based on Bit-Vectors.
The seminar will also report on the support provided by TOrPEDO for reasoning on incomplete and partial models, where property satisfaction can depend on unknown parts of the model, and discuss how Topological Proofs can be transferred and adapted to other settings, e.g., to generate diagnostic information for signal-based temporal properties.
Finally, the seminar will reflect on the desire and the challenges to reach the Independence Day of witnessing the correctness of systems, when formalisms-independent frameworks can witness the correctness of different software artifacts.
About the speaker
Claudio Menghi
Claudio Menghi received his BSc and MSc degrees in computer science from the Politecnico di Milano, where he later obtained his Ph.D. degree under the supervision of Prof. Carlo Ghezzi in 2015.
He was a Postdoctoral Researcher at the University of Gothenburg and Chalmers (2017-2018), a Research Associate at the Interdisciplinary Centre for Security, Reliability and Trust, University of Luxembourg (2018-2021), and an Assistant Professor at McMaster University (2021-2022). He is an Assistant Professor at the University of Bergamo and an Adjunct Professor at McMaster University (2023-now).
Claudio Menghi's research interests are formal methods and software engineering, focusing on cyber-physical systems, robotics, and formal verification. He has spent several years doing research with industry and applying formal methods and software engineering techniques in real-world and industrial contexts.
He has led research projects with four industry partners: BOSCH and PAL Robotics in the robotics domain and LuxSpace and QRA Corp in the aerospace and cyber-physical domain.
Our events are for adults aged 16 years and over.
BCS is a membership organisation. If you enjoy this event, please consider joining BCS. You’ll be very welcome. You’ll receive access to many exclusive career development tools, an introduction to a thriving professional community and also help us Make IT Good For Society. Join BCS today
This event is brought to you by: BCS FACS (Formal Aspects of Computing Science) specialist group
