ABSTRACT. Modern computing systems increasingly involve autonomous agents acting concurrently, often either competing or collaborating to achieve differing objectives. Game-theoretic approaches offer a natural way to reason about the subtle behaviour of these systems. A further challenge is the need for probabilistic modelling: consider a multi-robot team operating in a noisy, uncertain environment, or a distributed network protocol employing randomisation. For these cases, stochastic games area powerful modelling formalism. But until recently practical tools and techniques for formal verification using these models have been lacking.

In this talk, we summarise the development of techniques for formal verification using stochastic games, and the associated model checking tool PRISM-games. We express quantitative correctness properties intemporal logic, and automatically synthesise strategies for agents which provide probabilistic guarantees on their correct behaviour. We describe recent advances in this area, including the use of concurrent stochastic games, for more realistic modelling of agents interacting concurrently, and Nash equilibria, for modelling multiple distinct agent objectives. We illustrate these techniques with examples from a range of applications, and also identify some of the future challenges that exist in the area.

ABSTRACT. In the SMT(LRA) learning problem, the goal is to learn SMT(LRA) constraints from real world data. To improve the scalability of SMT(LRA) learning, we present a novel approach called SHREC which uses hierarchical clustering to guide the search, thus reducing runtime. A designer can decide between higher quality (SHREC1) and lower runtime (SHREC2) according to their needs. Our experiments show a significant scalability improvement and only a negligible loss of accuracy compared to the current state-of-the-art.

ABSTRACT. Model learning (a.k.a. active automata learning) is a highly effective technique for obtaining black-box finite state models of software components. Thus far, generalisation to infinite state systems with in- puts/outputs that carry data parameters has been challenging. Existing model learning tools for infinite state systems face scalability problems and can only be applied to restricted classes of systems (register automata with equality/inequality). In this article, we show how we can boost the performance of model learning techniques by extracting the constraints on input and output parameters from a run, and making this grey-box information available to the learner. More specifically, we provide new implementations of the tree oracle and equivalence oracle from RALib, which use the derived constraints. We extract the constraints from runs of Python programs using an existing tainting library for Python, and compare our grey-box version of RALib with the existing black-box version on several benchmarks, including some data structures from Python’s standard library. Our proof-of-principle implementation results in almost two orders of magnitude improvement in terms of numbers of inputs sent to the software system. Our approach, which can be generalised to richer model classes, also enables RALib to learn models that are out of reach of black-box techniques, such as combination locks.

ABSTRACT. This paper studies satisfaction of temporal properties on unknown stochastic processes that have continuous state spaces. We show how reinforcement learning (RL) can be applied for computing policies that are finite-memory and deterministic using only the paths of the stochastic process. We address properties expressed in linear temporal logic (LTL) and use their automaton representation to give a path-dependent reward function maximised via the RL algorithm. We develop the required assumptions and theories for the convergence of the learned policy to the optimal policy in the continuous state space. To improve the performance of the learning on the constructed sparse reward function, we propose a sequential learning procedure based on a sequence of labelling functions obtained from the positive normal form of the LTL specification. We use this procedure to guide the RL algorithm towards a policy that converges to an optimal policy under suitable assumptions on the process. We demonstrate the approach on a 4-dim cart-pole system and 6-dim boat driving problem.

ABSTRACT. In order to leverage the capacities of non-linear constraint solvers, we propose a reformulation of SAT into a box-constrained optimization problem where the objective function is polynomial. We prove that any optimal solution of the numerical problem corresponds to a solution of the Boolean formula, and demonstrate a stopping criterion that can be used with a numerical solver.

ABSTRACT. In this paper, we take technical and practical steps towards the modularisation of compliant-by-design executable declarative process models. First, we demonstrate by example how the specific language of timed DCR graphs is capable of modelling complex legislation, with examples from laws regulating the functioning of local governments in Denmark. We then identify examples of law paragraphs that are beyond these modelling capabilities. This incompatibility arises from subtle and---from a computer science perspective---non-standard interactions between distinct paragraphs of the law, which must then become similar interactions between model fragments. To encompass these situations, we propose a notion of /networks of processes/, where the processes are allowed to interact and regulate their interaction through the novel mechanisms of /exclusion/ and /linking/. Networks are parametric in the underlying process formalism, allowing interactions between processes specified in arbitrary and possibly distinct trace-language semantics formalisms as the individual models. Technically, we provide a sufficient condition for a good class of network compositions to realise /refinement/ of the constituent processes. Finally, parts of the theoretical framework (networks and exclusion) have been implemented by our industry partners, and we report on a preliminary evaluation suggestion that inter-model synchronisation is indeed both necessary and helpful in practical modelling scenarios.

ABSTRACT. Execution of Domain Specific Languages (DSL) is an active research area in Model Driven Engineering (MDE), whose intention is to perform early analysis of a system's behavior. Indeed, an executable DSL can be simulated and debugged by existing MDE-based tools leading to a better quality than a static DSL. Unfortunately, although these advantages show that executable DSLs are a promising paradigm, several issues related to correctness and the level of trust that one can have in execution engines are still challenging for a rigorous development process. In order to apply DSL execution in safety-critical systems we developed Meeduse, a tool in which the MDE paradigm is mixed with a formal method. Meeduse assists the formal definition of the DSL static semantics by translating its meta-model into an equivalent formal B specification. The dynamic semantics can be defined using proved B operations that guarantee the correctness of the DSL's behavior with respect to its safety invariant properties. Regarding execution, Meeduse applies the ProB animator in order to animate underlying domain-specific scenarios.

ABSTRACT. Over the years, researchers have developed many formal method tools to support software development. However, hardly any studies are conducted to determine whether the actual problems developers encounter are sufficiently addressed. For the relatively young field of GPU programming, we would like to know whether the tools developed so far are sufficient, or whether some problems still need attention. To this end, we first look at what kind of problems programmers encounter in OpenCL and CUDA. We gather problems from Stack Overflow and categorise them with card sorting. We find that problems related to memory, synchronisation of threads, threads in general and performance are essential topics. Next, we look at (verification) tools in industry and research, to see how these tools addressed the problems we discovered. We think many problems are already properly addressed, but there is still a need for easy to use sound tools. Alternatively, languages or programming styles can be created, that allows for easier checking for soundness.

ABSTRACT. In floating-point programs, test instability occurs when the control flow of a conditional statement diverges from its ideal execution under real arithmetic. This phenomenon is caused by the presence of round-off errors in floating-point computations. Writing programs that correctly handle test instability often require expertise on finite precision computations and rounding errors. This paper presents a fully automatic toolchain that generates and formally verifies a test-stable floating-point C program from its functional specification in real arithmetic. The generated program is instrumented to soundly detect when unstable tests may occur and, in these cases, to issue a warning. The proposed approach combines the PRECiSA floating-point static analyzer, the Frama-C software verification suite, and the PVS theorem prover.

ABSTRACT. We present Jaint, a generic security analysis for JAVA Web-applications that combines concolic execution and dynamic taint analysis in a modular way. Jaint executes user-defined taint analyses that are formally specified in a domain-specific language for expressing taint-flow analyses. We demonstrate how dynamic taint analysis can be integrated into jDart, a dynamic symbolic execution engine for the Java virtual machine in Java PathFinder. The integration of the two methods is modular in the sense that it traces taint independently of symbolic annotations and thus is capable of sanitizing taint information (if specified by a taint analysis) and using multi-colored taint for running multiple taint analyses in parallel. We design a domain-specific language (using the Meta Programming System (MPS)) that enables users to define specific taint-based security analyses, e.g., for Java Web-applications. Specifications in this domain-specific language serve as a basis for the automated generation of corresponding taint injectors, sanitization points and taint-flow monitors that implement taint analyses in Jaint. We demonstrate the generality and effectiveness of the approach by analyzing the OWASP benchmark set, using generated taint analyses for all 11 classes of CVEs in the benchmark set.