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.

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.