ICTAC 2023 Training School on Applied Formal Methods
About the school
Formal Methods are logic-based techniques for the specification, development, and verification of systems. They contribute to the reliability and trustworthiness of systems and they deal with models of systems that capture their dynamic aspects (e.g., processes, transitions) and their properties (e.g, safety, liveness, fairness).
The ICTAC training school on applied formal methods will be held in Lima - Peru at UTEC, December 04-05, 2023 and it targets master students, Ph.D. students, early-stage researchers, and lectures 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. We plan to do so, via various lectures on selected formal methods.
There is a limited number of free registrations, sponsored by SIGSOFT, and a limited number of registrations with a minimum payment for Peruvian residents/citizens. Please contact Cristian Lopez del Alamo (clopezd@utec.edu.pe) for further information.
Speakers
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.
Lecturer Sponsored by The ICT faculty at The University of Malta
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.
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.
Satisfiability Solving.
Satisfiability (SAT) solvers have become powerful search engines to solve a wide range of applications in fields such as formal verification,
planning, and mathematics. This lecture on SAT solving consists of two parts. The first part focuses on an introduction that ranges from many
applications of SAT to interesting theoretical aspects. It also covers basic solving techniques.
The second part provides hands-on experience on how to use SAT solvers in practice. This part consists of various examples,
such as how to encode a graph coloring problem into SAT and solving the resulting formula with a top-tier solver.
Additionally, we demonstrate some tools to make it easier to use SAT. We conclude by presenting satisfiability modulo theory (SMT)
solvers and how they can be used to solve problems.
Lecture Sponsored by FME (Formal Methods Europe) and
The University of York
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.
Name: Ziggy Attala
Affiliation: University of York, United Kingdom
Homepage: https://www.cs.york.ac.uk/people/?username=ziggy
Bio:
Ziggy Attala is currently finishing his Ph.D. in the verification of RoboChart models with integrated artificial neural network
components at the University of York, supervised by Ana Cavalcanti and Jim Woodcock.
His undergraduate dissertation, supervised by Arno Pauly in Swansea University, concerned how machine learning models can
outlearn and recognize other machine learning models. His research interests include formal methods,
machine learning, and the verification of artificial neural networks.
Name: Jim Woodcock
Affiliation: University of York, United Kingdom
Homepage: https://pure.york.ac.uk/portal/en/persons/jim-woodcock
Bio:
Jim Woodcock is the Anniversary Professor of Software Engineering at the University of York, a Fellow of the Royal Academy of Engineering,
a Chartered Engineer, a Chartered IT Professional, and an award-winning researcher and teacher.
He is also the Professor of Software Engineering of Mobile and Autonomous Robots at Aarhus University and Professor of Cyber-Physical
Systems at China's Southwest University. He has 45 years of experience in formal methods and has dedicated his research career to
searching for the mathematical principles that are essential to the practice of software engineering. His specific research interests
are in unifying theories of programming (UTP), robotics, digital twins, and industrial applications. He leads the team creating UTP
theories for state-rich concurrent programming, including timing and probability and is developing the Isabelle/UTP theorem prover.
He applied the Z notation to the IBM CICS project, helping to gain a Queen's Award for Technological Achievement.
He created the theory and practical verification for NatWest Bank's Mondex smartcard system, the first commercial product
to achieve ITSEC Level E6 (Common Criteria EAL 7). For the last decade, he has researched the theory and practice of cyber-physical
systems and robotics and, recently, their probabilistic semantics. He is Editor-in-Chief of the ACM journal Formal Aspects of
Computing and Editor-in-Chief of the CUP journal Research Directions: Cyber-Physical Systems.
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.