ABSTRACT. Probabilistic programming is the idea of writing models from statistics and machine learning using program notations and reasoning about these models using generic inference engines. Recently its combination with deep learning has been explored intensely, which led to the development of so called deep probabilistic programming languages, such as Pyro, Edward and ProbTorch. At the core of this development lie inference engines based on stochastic variational inference algorithms. When asked to find information about the posterior distribution of a model written in such a language, these algorithms convert this posterior-inference query into an optimisation problem and solve it approximately by a form of gradient ascent or descent. In this paper, we analyse one of the most fundamental and versatile variational inference algorithms, called score estimator or REINFORCE, using tools from denotational semantics and program analysis. We formally express what this algorithm does on models denoted by programs, and expose implicit assumptions made by the algorithm on the models. The violation of these assumptions may lead to an undefined optimisation objective or the loss of convergence guarantee of the optimisation process. We then describe rules for proving these assumptions, which can be automated by static program analyses. Some of our rules use nontrivial facts from continuous mathematics, and let us replace requirements about integrals in the assumptions, such as integrability of functions defined in terms of programs' denotations, by conditions involving differentiation or boundedness, which are much easier to prove automatically (and manually). Following our general methodology, we have developed a static program analysis for the Pyro programming language that aims at discharging the assumption about what we call model-guide support match. Our analysis is applied to the eight representative model-guide pairs from the Pyro webpage, which include sophisticated neural network models such as AIR. It finds a bug in two of these cases, and shows that the assumptions are met in the others.

This is joint work with Wonyeol Lee (Stanford, USA) and Hangyeol Yu (Riiid, South Korea) and Xavier Rival (INRIA Paris/CNRS/ENS/PSL Research University, France).

ABSTRACT. We present a method for synthesizing loops over affine assignments from polynomial invariants. It is complete when the number of auxiliary variables is bounded, thus serving as a foundation for strength reduction optimization that convert polynomial expressions into incremental affine computations. Our work has applications towards synthesizing loops satisfying a given polynomial loop invariant, program verification, as well as generating number sequences from algebraic relations. To understand viability of the methodology and heuristics for synthesizing loops with a large number of auxiliary variables, we implement and evaluate the method using the Absynth tool.

ABSTRACT. The theory of Communicating Sequential Processes going back to Hoare and Roscoe is always a reference model for concurrent specification and computing. In 1997, a first formalization in Isabelle/HOL of the denotational semantics of the Failure/Divergence Model of CSP was undertaken; in particular, this model can cope with infinite alphabets, in contrast to model-checking approaches limited to finite ones. In this paper, we extend this theory to a significant degree by taking advantage of more powerful automation of modern Isabelle version, which came even closer to recent developments in the semantic foundation of CSP.

More importantly, we use this formal development to analyse a family of refinement notions, comprising classic and new ones. This analysis enabled us to derive a number of properties that allow to deepen the understanding of these notions, in particular with respect to specification decomposition principles in the infinite case. Better definitions allow to clarify a number of obscure points in the classical literature, for example concerning the relationship between deadlock- and livelock-freeness. As a result, we have a modern environment for formal proofs of concurrent systems that allow to combine general infinite processes with locally finite ones in a logically safe way.

We demonstrate a number of resulting verification-techniques for classical, generalized examples: The CopyBuffer and Dijkstra's Dining Philosopher Problem of an arbitrary size.

ABSTRACT. We propose a technique to automatically generate a formal specification of the model of a system from a set of observations of its behaviour. We aim to free systems modellers from the burden of explicitly formalising the behaviour of an existing system to analyse it. We take advantage of an algorithm introduced by the process mining community, which takes as input an event log and generates a formal specification that can be combined with other specifications to obtain a global model of the overall behaviour of a system. Specifically, we have adapted a known process discovery algorithm to produce a specification in mCRL2, a formal specification language based on process algebras. The availability of mCRL2 specifications enables us to take advantage of its rich toolset for verifying systems properties and for effectively reasoning over distributed scenarios where multiple organizations interact to reach common goals. This is an aspect that is not supported by the approaches based on Petri Nets, usually used for process mining. The methodology has been integrated in a stand-alone tool and has been validated using custom-made and real event logs.

ABSTRACT. This paper presents an approach to generate SPARK code from Event-B models. System models in Event-B are translated into SPARK packages including proof annotations. Properties of the Event-B models such as axioms and invariants are also translated and embedded in the resulting models as pre- and post-conditions. This helps with generating SPARK proof annotations automatically hence ensuring the correct behaviour of the resulting code. A prototype plug-in for the Rodin has been developed and the approach is evaluated on different examples. We also discuss the possible extensions including to generate scheduled code and data structures such as records.

ABSTRACT. Designing hybrid systems requires the handling of discrete and continuous behaviours. The formal verification of such systems revolves around the use of heavy mathematical features, and related proofs. This paper presents a generic and reusable framework with different patterns, aimed at easing the design and verification of hybrid systems. It relies on refinement and proofs using Event-B, and defines an easily extensible set of generic patterns in the form of theories and models that are proved once and for all. The model of any specific hybrid system is then produced by instantiating the corresponding patterns. The paper illustrates the use of this framework by proposing to realise a well-known case study of the inverted pendulum, which design uses the approximation pattern formally defined and verified in Event-B.

ABSTRACT. Well-Definedness is important for many formal methods. In B and Event-B it ensures that certain kinds of errors (e.g., division by 0) cannot appear and that proof rules based on two-valued logic are sound. For validation tools such as ProB, well-definedness is also important for constraint solving, in particular when dealing with quantifiers or set comprehensions. B and Event-B establish well-definedness by generating dedicated proof obligations (POs). Unfortunately, the standard provers are often not very good at discharging them. In this paper, we present a new integrated technique to simultaneously generate and discharge well-definedness POs. The implementation contains a dedicated rule-based prover written in Prolog and supports B, Event-B and extensions thereof for data validation. We show that the generation and discharging is significantly faster than existing implementations in Rodin and Atelier-B and we show that a large number of POs are automatically discharged. The POs are also fine-grained enough to provide precise source code feedback, and allow inspection of problematic POs within various editors.