Abstract: In this talk we give an introduction to Mirrorsolve, a Coq library for solving Coq proofs using SMT solvers. Foundational theorem provers such as Isabelle/HOL and Coq are the gold standard for building certified systems, enabling the verification of extremely rich properties while having a minimal trusted code base. Unfortunately, these provers come with […]

Abstract: We will give a general introduction to Gillian, a platform for the development of symbolic-execution tools for many programming languages.  Gillian currently supports three types of analysis: whole-program symbolic testing; full verification based on separation logic; and automatic compositional testing based on bi-abduction. It uses a core symbolic execution engine with strong mathematical foundations […]

Abstract: Advances in deep neural networks (DNNs) have increased their deployment in safety-critical systems, such as vision perception modules for autonomous vehicles and airborne collision avoidance system controllers for unmanned aircraft. Modern DNNs and linear classifiers are susceptible to adversarial input perturbations. Adversarial perturbations are small changes to an input that result in unexpected changes […]

Abstract:Formal verification has become a well-established part of standard hardware design flows leveraging SAT solvers and model checkers for verification tasks including logical equivalence checking, property checking, and protocol verification. These tools are largely based on all-digital, synchronous, single clock-domain models of hardware behaviour. To address the needs of system-on-chip and multi-core designs, we are […]

abstract: We are at the dawn of a new age in air traffic control. The airspace is full in the sense that demand for flights exceeds our capacity to add new air traffic. The time-tested current method of air traffic control has hit its scalability limit and must be replaced with a new system that […]

abstract: Software-dependent critical systems that impact daily life are rapidly increasing in number, size, and complexity. Unfortunately, inadequate software and systems engineering can lead to accidents that cause economic disaster, injuries, or even death. There is a growing reliance on development and verification tools to reduce costs, better manage complexity, and to increase confidence in […]

abstract: Modern verification techniques are becoming ever-more powerful and sophisticated, and building tools to implement them is a time-consuming and difficult task. Writing a new verifier to validate each on-paper approach is impractical; for this reason intermediate verification languages such as Boogie and Why3 have become popular over the last decade for implementing research from […]

abstract: Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested and subject to priorities. Interrupts can arrive at arbitrary times, leading to an explosion in the number of cases to be considered. We present a new formal approach to verifying interrupt-driven software based on symbolic execution. The approach leverages recent […]

abstract: Read-copy update (RCU) is a synchronization mechanism that is sometimes used as an alternative to reader-writer locking (among other things) that was added to the Linux kernel in 2002. A similar mechanism was added to Sequent’s DYNIX/ptx parallel UNIX kernel in 1993, and antecedents go back to at least 1980. Although a fully functional […]

Abstract Cyber-Physical Systems (CPS) refer to systems in which control, computation and communication converge to achieve complex functionalities. The ubiquitous deployment of cyber-physical systems in safety critical applications including aeronautics, automotive, medical devices and industrial process control, has pressurized the need for the development of automated analysis methods to aid the design of high-confidence systems. The talk will focus on an […]