Title:Dynamic Symbolic Execution for Software Analysis
Speaker: Cristian Cadar, Imperial College London
Abstract:Symbolic execution is a program analysis technique that can automatically explore and analyse paths through a program. While symbolic execution was initially introduced in the seventies, it has only received significant attention during the last decade, due to tremendous advances in constraint solving technology and effective blending of symbolic and concrete execution into what is often called dynamic symbolic execution. Dynamic symbolic execution is now a key ingredient in many computer science areas, such as software engineering, computer security, and software systems, to name just a few.
In this talk, I will discuss recent advances and ongoing challenges in the area of dynamic symbolic execution, drawing upon our experience developing several symbolic execution tools for many different problems, such as high-coverage test input generation, bug and security vulnerability detection, patch testing and bounded verification, among many others.
Title: Integrating formal methods for modelling and simulation of swarm robotics
Speaker: Ana Cavalcanti, University of York
There are many challenging aspects involved in ensuring safety of mobile and autonomous robots. One aspect that has been neglected is software engineering. The state-of-practice uses costly iterations of trial and error, often with hardware and environment in the loop, after an ad hoc use of simulations. It is clear that the modern outlook of the robotic applications is not matched by the outdated practices of design and verification when it comes to controller software.
We present two new domain-specific languages for robotics: RoboChart and RoboSim. They support a model-based approach for early formal validation and sound generation of simulations. In robotics, simulation is the favoured technique for analysis. In our work, simulation is complemented by analysis based on model checking, using CSP, tock-CSP, and the refinement model checker FDR, and theorem proving, using Isabelle/UTP. Our ultimate goal is to support reasoning and code generation using a variety of techniques, but relying on theorem proving to deal with data-rich and large systems, especially with models for swarm applications.
RoboChart is a UML-like notation that includes timed and probabilistic primitives for modelling of controllers. We link it to RoboSim, another graphical notation defined as a gateway between RoboChart models and customised simulations developed for traditional robotics simulators. RoboChart enforces design patterns appropriate to deal with robotic applications and now includes also notation to model collections of robots as present in swarms.
Our approach is predicated on a few principles. First, we adopt notations akin to those in current use by practitioners, namely, notations based on state machines, to ensure usability. Second, we enforce specific architectural patterns relevant for the area, and define precise languages that can be used for automatic generation of mathematical models. Third, our goal is to hide the formalisms from practitioners entirely. Via specialisation and automation, we seek both scalability and usability. Finally, we investigate the integrated use of a variety of techniques together to tackle the different needs of verification and development.
Title: Program Correctness under Weak Memory Consistency
Speaker: Viktor Vafeiadis, MPI-SWS
It is fairly common knowledge that shared-memory concurrent programs running on modern multicore processors do not adhere to the interleaving concurrency model, but rather exhibit weakly consistent behaviours, such as store and load buffering. Formally, the semantics of shared-memory concurrent programs is determined by a weak memory model, defined either by the programming language (e.g., in the case of C/C++11 or Java) or by the hardware architecture (e.g., for assembly and legacy C code).
These weak memory models pose two major challenges for software verification. First, many standard proof techniques that were developed for interleaving concurrency, such as the Owicki-Gries method, are unsound in the context of weak memory consistency. Second, it is not even clear how to specify the correctness of concurrent libraries when there is no globally agreed notion of time and state. To overcome these challenges, we therefore have to develop new techniques for specifying and verifying weakly consistent concurrent programs. The invited talk will present some first steps in this direction.