Name: Marijn J.H. Heule
Affiliation: Carnegie Mellon University, USA
Homepage: https://www.cs.cmu.edu/~mheule/

Bio:
Marijn Heule is an Associate Professor of Computer Science at Carnegie Mellon University. His contributions to automated reasoning have enabled him and others to solve hard problems in formal verification and mathematics. He has developed award-winning satisfiability (SAT) solvers. His preprocessing and proof-producing techniques are used in many state-of-the-art automated reasoning tools. Marijn won multiple best paper awards at international conferences, including at SAT, CADE, IJCAR, TACAS, HVC, LPAR, and IJCAI-JAIR. He is one of the editors of the Handbook of Satisfiability. This 1500+ page handbook (second edition) has become the reference for SAT research.

Topic of the Lecture: TBD

Name: Ana Cavalcanti
Affiliation: University of York, United Kingdom
Homepage: https://www-users.york.ac.uk/~alcc500/

Bio:
Ana Cavalcanti is a Professor at the University of York and a Royal Society - Wolfson Research Merit Award holder. In 2003, she was awarded a Royal Society Industry Fellowship to work with QinetiQ on formal methods. She has published more than 100 papers and chaired the Programme Committee of various well-established international conferences. Her main research interest is the theory and practice of formal methods. She has a long-term interest in refinement, safety-critical systems, object-orientation , concurrency, and real-time applications. She has played a major role in the design and formalization of a state-rich process algebra, namely, Circus, and its development techniques using Hoare and He’s Unifying Theories of Programming.

Software Engineering for Robotics: RoboStar technology
The use of simulations to support the design of software for robotic systems is pervasive. Typically, roboticists draw a state machine using an informal notation (not precise or machine-checkable) to convey a design and guide the development of a simulation. This involves writing code for a specific simulator (using C, C++, or some proprietary language and API). Reactive robotics simulators do not normally generate code for deployment. Instead, simulation code is often reused after changes. So, there is a potential loss of properties observed via simulation: because of the possibility of changes introducing errors, and because of the reality gap. The RoboStar technology supports a model-based, rather than (simulation) code, approach to development. Models are written using domain-specific notations in line with those accepted by roboticists. In this lecture, we will focus on modelling and verification using RoboChart, our design notation, and its tool. In RoboChart, software controllers are described by timed state machines. The semantics is defined using a process algebra, namely, tock-CSP, which we use for verification.

Name: Pedro R. D'Argenio
Affiliation: National University of Córdoba, Argentina
Homepage: https://cs.famaf.unc.edu.ar/~dargenio/

Bio:
Pedro R. D'Argenio is a Full Professor in Computer Science at FAMAF, National University of Córdoba. He also holds a research post at CONICET. He studied computer science at the National University of La Plata (Argentina), and obtained his Ph.D. at the University of Twente (Netherlands) where he also did his postdoc. He has also worked at the Université de Provence (FR), and was Visiting Professor at the University of Twente (NL) and Saarland University (DE). He is a former Director of the Doctoral Program in Computer Science and former Associate Dean of Science and Technology at FAMAF, UNC. He is currently the Chair of the IFIP WG 1.8 on Concurrency Theory. Prof. D'Argenio is a leading researcher in formal techniques for dependable systems, contributing in areas such as model checking, process semantics, fault tolerance, security, and testing. He has led and participated in numerous Argentine and European research projects.

Probabilistic Model Checking.
Model checking is a powerful tool to verify automatically if a model satisfies a given property. They normally provide a Boolean answer to a qualitative question. However, probabilistic features normally appear in systems of usually crucial characteristics. For example, it is common to use randomized protocols to solve contention situations in networks or to understand fault models through the stochastic behaviors of faults. In this last case, for instance, the statement "the system does not fail" might be impossible to verify while rather the appropriate question could be "99% of the time the system does not fail". In this tutorial, we will introduce the fundamentals and algorithms to address the verification of this type of quantitative properties. In particular, we will discuss the verification of quantitative and qualitative properties on discrete-time Markov chains as well as on the more versatile setting of Markov decision process.

Name: Christian Colombo
Affiliation: University of Malta, Malta
Homepage: https://www.um.edu.mt/profile/christiancolombo

Bio:
Christian Colombo obtained his Ph.D. in Computer Science from the University of Malta in 2013 and currently holds the position of Associate Professor within the Department of Computer Science. His main areas of research are runtime verification, software testing, compensating transactions, and domain-specific languages, focusing on the creation of dependable software systems by verifying them against formal specifications at runtime. The applications of this body of research span mobile device security, payment gateway systems, social network privacy policies, and tax compliance, amongst others. He is actively involved in outreach activities both at the department and faculty level, engaging with potential future students, industry, and the general public. He has been closely involved in a number of funded projects: Dependability and Error-Recovery in Security Intensive Financial Systems [MCST] (2008-2011), Open Payments Ecosystem [H2020] (2015-2017), Generating Online Monitors from Tests Automatically [MCST] (2015-2017); LOCARD [H2020-SU-SEC-2018: 832735] (2019-2022), Secure Communication in the Quantum Era [SPS Project Number: G5448] (2018-2022), and DETECTIF [MCST REP-2022-007] (2022-2023).

The Theory and Practice of Runtime Verification:
A Hand-On Introduction to the Formal Methods Technique with Applications in Cyber Security Monitoring
Runtime verification is a lightweight formal methods technique that synthesizes executable monitors from unambiguous behavior descriptions. Such monitors are then automatically combined with the system under scrutiny to check its correctness at runtime. Drawing on two decades of experience, this session will start by covering the theoretical bases of runtime verification, particularly the specification and detection of any behavior violations at runtime. Next, we will have a hands-on session where participants will be invited to try out Java and AspectJ code in their IDEs, using a financial transaction case study (see https://github.com/ccol002/rv-book if you are curious!). The last part of the session will focus on runtime verification in the context of cybersecurity; showing how it can monitor the execution of security protocols, enforce isolation of a trusted execution environment, and extract evidence that would otherwise be hard to obtain.