FM 2016 | Tutorials

Tutorials at FM 2016

Program and Additional Information

TUTORIAL	MONDAY, 7 NOVEMBER	TUESDAY, 8 NOVEMBER
Abstraction and Rely/Guarantee Thinking	√ (Half Day - AM)
KeYmaera X Tutorial - Tactics and Proofs for Cyber-Physical Systems	√ (Half Day - PM)
Session Types for Concurrent and Distributed Programming: Principles and Practice	√ (Half Day - PM)
Cyber-Physical Systems Engineering: Next Generation Foundations, Methods and Tools		√ (Full Day)
The CProver Suite of Verification Tools		√ (Half Day - AM)

Monday 7, November

Abstraction and Rely/Guarantee Thinking

Tutors:

Cliff Jones, Newcastle University, GB
Ian Hayes, University of Queensland, AU

Brief Description:

The general view of rely/guarantee thinking appears to apply to a very wide range of applications: it facilitates the development and formal proof of intricate code — at the other extreme, it provides a framework for deriving the specification of control systems that respond to –and actuate– physical systems that interact with the physical world. In the last couple of years, the way of recording rely assumptions and guarantee commitments has been recast into a style similar to the refinement calculus. This results in a much more algebraic feel to reasoning about rely/guarantee thinking and the laws of this calculus will be explained and demonstrated on examples. There are intriguing links between rely/guarantee thinking and separation logic and these will also be explored.

KeYmaera X Tutorial - Tactics and Proofs for Cyber-Physical Systems

Tutors:

Stefan Mitsch, Carnegie Mellon University, US
Nathan Fulton, Carnegie Mellon University, US
André Platzer, Carnegie Mellon University, US

Brief Description:

Cyber-physical systems that combine discrete and continuous dynamics are everywhere including automatic or semi-automatic controllers in modern (self-driving) cars, trains, airplanes, ground robots, robotic household appliances, or surgical robots. This tutorial will introduce the new theorem prover KeYmaera X to establish safety properties that reason about the interaction between software and the physical real world encountered in modern cyber-physical systems. You will learn how to model software together with physics and verify safety properties formally (e.g., a robot will not collide with obstacles).

More information about the tutorial can be found here

Session Types for Concurrent and Distributed Programming: Principles and Practice

Tutors:

Raymond Hu, Imperial College London, GB
Jorge A. Pérez, University of Groningen, GB
Nobuko Yoshida, Imperial College London, GB

Brief Description:

Concurrency and distribution are two of the most pressing challenges in the IT landscape nowadays. Many programmers must routinely write code that involves the interaction with distributed components (Web applications, cloud-based services); to avoid insidious and costly bugs, it is critical that such interactions precisely follow communication structures, or protocols. These protocols are naturally concurrent, and therefore intrinsically complex; this calls for rigorous approaches for validating communicating programs against specifications of interaction protocols.

Session types have consolidated as a rigorous, paradigm-independent methodology for validating communicating programs, supported by solid formal foundations and available to practitioners in the form of practical tools and languages. The tutorial will cover the principles of session type disciplines, and will showcase the latest advances on practical support for session type validation, as implemented in the Scribble protocol language and its applications.

Tuesday 8, November

Cyber-Physical Systems Engineering: Next Generation Foundations, Methods and Tools

Tutors:

John Fitzgerald, Newcastle University, GB
Peter Gorm Larsen, Aarhus University, DK
Jim Woodcock, University of York, GB
Ken Pierce, Newcastle University, GB
Simon Foster, University of York, GB

Brief Description:

Some of the most exciting challenges in modern systems engineering are presented by Cyber-Physical Systems (CPSs). Characterised by close interaction between computing and physical processes, and requiring distributed control, examples include building automation, transport and agriculture. Because the system of interest includes both cyber and physical elements, CPS engineers need tools that cross the boundaries between established, but very different, engineering disciplines. There have been major research investments in this area, and in this tutorial, we offer an update on the state of the art in integrating diverse engineering techniques in a practically effective but semantically well-founded way. Participants will get hands-on experience with new design tools that are also being piloted in industry, and will have an opportunity to see how an extensible semantic platform can put CPS engineering on a sound footing by applying Unifying Theories of Programming.

The CProver Suite of Verification Tools

Tutors:

Daniel Kroening, University of Oxford, GB
Martin Brain, University of Oxford, GB
Peter Schrammel, University of Sussex, GB

Brief Description:

Want to use automated verification tools to improve the quality of your software and system? Curious about the state-of-the-art and practice in automated formal verification of software? Want to work on verification but don't want to build all of the infrastructure? This tutorial can help! We will give an introduction to the CPROVER suite of verification tools one of the largest, most established and powerful automatic verification systems for C, C++, Verilog, Java and more.