ABSTRACT. Deep Neural Networks (DNNs) are increasingly used in a variety of applications that require high assurance guarantees. Verification and understanding of DNNs is hindered by their high complexity, their opaqueness and sensitivity to small adversarial perturbations and also by the lack of high-level formal specifications. In this talk I will describe recent research work which explores techniques and tools to ensure that DNNs and systems that use DNNs are safe, robust and interpretable. Research directions we are pursuing include: symbolic execution for DNN analysis, compositional approaches to improve formal SMT-based verification, property inference for DNNs, adversarial training and detection, and probabilistic reasoning for DNNs. The techniques aim to provide strong guarantees wrt safety and robustness for DNNs, making them amenable for use in safety critical domains, particular autonomy. We have applied our techniques to the analysis of deep neural networks designed to operate as controllers in the next-generation Airborne Collision Avoidance Systems for unmanned aircraft (ACAS Xu). We have also studied image classification networks (MNIST, CIFAR) and sentiment networks (for text classification).

Corina Pasareanu is a distinguished researcher at NASA Ames and Carnegie Mellon University. She is affiliated with CMU’s CyLab and holds a courtesy appointment in Electrical and Computer Engineering. At Ames, she is developing and extending Symbolic PathFinder, a symbolic execution tool for Java bytecode. Her research interests include model checking and automated testing, compositional verification, model-based development, probabilistic software analysis, and autonomy and security. She is the recipient of several awards, including ASE Most Influential Paper Award (2018), ESEC/FSE Test of Time Award (2018), ISSTA Retrospective Impact Paper Award (2018), ACM Distinguished Scientist (2016), ACM Impact Paper Award (2010), and ICSE 2010 Most Influential Paper Award (2010). She has been serving as Program/General Chair for several conferences including: ICST 2020, ESEC/FSE 2018, CAV 2015, ISSTA 2014, ASE 2011, and NFM 2009. She is currently an associate editor for the IEEE TSE journal.

ABSTRACT. Various relations have been defined to express refinement and conformance for state-transition systems with inputs and outputs, such as ioco and uioco in the area of model-based testing, and alternating simulation and alternating-trace containment originating from game theory and formal verification. Several papers have compared these independently developed relations, but these comparisons make assumptions (such as input-enabledness), pose restrictions (such as determinism -- then they all coincide), use different models (such as interface automata and Kripke structures), or do not deal with the concept of quiescence. In this paper, we present the integration of the ioco/uioco theory of model-based testing and the theory of alternating refinements, within the domain of non-deterministic, non-input-enabled interface automata. A standing conjecture is that ioco and alternating trace containment coincide. Our main result is that this conjecture does not hold, but that uioco coincides with a variant of alternating-trace containment, for image finite interface automata and with explicit treatment of quiescence. This result is based on a particular translation of the game-theoretic notion of alternating-trace containment from Kripke structures to the setting of interface automata. From the comparison between ioco-theory and alternating refinements, we conclude that ioco and the original relation of alternating trace containment are too strong for realistic black-box scenarios.

ABSTRACT. In the traditional workflow of high-level specification languages such as B, code is refined in many steps until a small "implementable" subset of the language is reached. Then, code generators are used to derive code from this implementation-level code, targeting traditional programming languages such as C or Ada.

In this paper, we pursue the aim to diminish the number of refinement steps needed, by providing a more powerful code generator. Indeed, many high-level data types and operations, such as sets, can already be translated to traditional programming languages such as Java and C++. We present a new code generator for B named B2Program with two distinct features. Firstly, it targets multiple high-level languages via a template-based approach to compilation. In addition to flexibility, this also enables one to safeguard against errors in the individual compilers and standard libraries, by generating multiple implementations of the same formal model. Secondly, it supports higher-level constructs compared to existing code generators. This enables new uses of formal models, as prototypes, demonstrators or simply as very high-level programming languages for productivity gains, by directly embedding formal models as components into software systems.

In the article, we discuss the implementation of our code generator, evaluate it using B models taken from literature and compare its performance with simulation in ProB.

ABSTRACT. The SMT-LIB language and the B language are both basedon predicate logic and share the definition of several operators. However, B supports data types not available in SMT-LIB and vice versa. In this article we suggest a straightforward translation from SMT-LIB to B. Using this translation, SMT-LIB can be analyzed by tools developed for the B method. We show how Atelier B can be used for automatic and interactive proof of SMT-LIB problems. Furthermore, we incorporated our translation into the model checker ProB and applied it to several benchmarks taken from the SMT-LIB repository. In contrast to most SMT solvers, ProB relies on finite domain constraint propagation, with support for infinite domains by keeping track of the exhaustiveness of domain variable enumerations. Our goal was to see whether this kind of approach is beneficial for SMT solving.

ABSTRACT. Numerical software uses floating-point arithmetic to implement real-valued algorithms which inevitably introduces roundoff errors. Additionally, in an effort to reduce energy consumption, approximate hardware introduces further errors. As errors are propagated through a computation, the result of the approximated floating-point program can be vastly different from the real-valued ideal one. Previous work on soundly bounding (roundoff) errors has focused on worst-case absolute error analysis. However, not all inputs and not all errors are equally likely such that these methods can lead to overly pessimistic error bounds.

In this paper, we present a sound probabilistic static analysis which takes into account the probability distributions of inputs and propagates roundoff and approximation errors probabilistically through the program. We observe that the computed probability distributions of errors are hard to interpret, and propose an alternative metric and computation of refined error bounds which are valid with some probability.

ABSTRACT. We are interested in describing timed systems that exhibit probabilistic behaviour and in evaluating their behavioural discrepancies. To this purpose, we consider probabilistic timed automata, we introduce a concept of $n$-bisimilarity metric and give an algorithm to decide it.

ABSTRACT. Probabilistic model checking (PMC) is a well-established method for the quantitative analysis of dynamic systems. On the other hand, description logics (DLs) provide a well-suited formalism to describe and reason about static knowledge, used in many areas to specify domain knowledge in an ontology. We investigate how such knowledge can be integrated into the PMC process, introducing ontology-mediated PMC. Specifically, we propose a formalism that links ontologies to dynamic behaviors specified by guarded commands, the de-facto standard input formalism for PMC tools such as Prism. Further, we present and implement a technique for their analysis relying on existing DL-reasoning and PMC tools. This way, we enable the application of standard PMC techniques to analyze knowledge-intensive systems. Our approach is implemented and evaluated on a multi-server system case study, where different DL-ontologies are used to provide specifications of different server platforms and situations the system is executed in.