We examine the problem of inferring invariants for parametrized systems. Parametrized systems are concurrent systems consisting of an a priori unbounded number of process instances running the same program. Such systems are commonly encountered in many situations including device drivers, distributed systems, and robotic swarms. In this talk, I will describe a technique that enables leveraging off-the-shelf invariant generators designed for sequential programs to infer invariants of parametrized systems. The central challenge in invariant inference for parametrized systems is that naïvely exploding the transition system with all interleavings is not just impractical but impossible. In our approach, the key enabler is the notion of a reflective abstraction that we prove has an important correspondence with inductive invariants. This correspondence naturally gives rise to an iterative invariant generation procedure that alternates between computing candidate invariants and creating reflective abstractions.

This is joint work with Sriram Sankaranarayanan, César Sánchez and Bor-Yuh Evan Chang.

Malware is a serious problem on mobile devices. Our vision is a verified app store in which each application has been formally proven to be free of (certain) defects and exploits. We have built such a system and successfully applied it to dozens of challenge applications created by hostile Red Teams. This talk describes our type system for information flow, along with support for implicit invocation (intents and reflection), varieties of polymorphism, and other challenges that arose.

In this talk we present the framework Failure Tabled Constraint Logic Programming by Interpolation, FTCLP (Gange et al. 2013), that, similarly to Tabled Constraint Logic Programming, TCLP (Codognet 1995; Chico et al. 2012), combines the benefits of constraints and tabling in Prolog. FTCLP learns from failed derivations in order to prune further derivations. This allows to compute interpolants rather than constraint projection (TCLP) for generation of reuse conditions. As a result this technique: can be used where projection is too expensive or does not exist; and speeds up the execution of programs with many redundant failed derivations. In the presence of infinite derivations due to recursive clauses, it uses iterative deepening search to terminate in more cases than the standard execution model of CLP. This framework is then applied to the verification of safety properties in C programs and the results are compared with Blast, HSF and Tracer. Finally, we describe some differences between FTCLP and TCLP.

In this talk we present a constraint logic framework that combines backward and forward chaining. Concretely in this framework coexist two kinds of rules: On the one some rules ---which corresponds to CLP clauses--- are processed by backward chaining, while on the other hand the others rules ---which generalize constraint propagation rules-- are processed by forward chaining. We then illustrate how commutation of the backward rules with respect to the forward rules can be used to automate inductive proofs over CLP programs.

In Service-Oriented Architecture (SOA), service compositions provide the key tool for building complex, flexible, distributed, and cross-boundary functionality from elementary services (and the composition can be exposed as services themselves). Yet, while conversion of atomic and back-end services from centralized servers to cloud platforms has been largely successful, the composition layer often remains a bottleneck due to the prevailing reliance on transactional state management.

The composition layer can be re-engineered for horizontal and vertical scalability by moving away from the concurrency model dominated by heavy-weight components (such as virtual machines and database transactions) towards a finer-grained model of concurrent and distributed computing based on actor systems.

In this talk we'll look at a scheme for automatically transforming the traditional (orchestration-style) service compositions into Cloud-friendly actor networks, which can benefit from high performance, location transparency, clustering, load balancing, and integration capabilities of modern actor systems, such as Akka.

Most logics for stateful reasoning in a concurrent setting are designed around a parallel composition operator ||. Given two programs p1 and p2, || composes them concurrently, creating a new program p1 || p2 where resources are shared amongst two threads, with p1 and p2 potentially racing for a shared resource. This syntactic, well-bracketed approach enables reasoning inductively and fosters modular reasoning, but it enforces a fixed synchronization pattern between the forked threads. On the other hand, in most real-world concurrent programming environments, threads are spawned dynamically using fork primitives. This practice allows for more flexible synchronization patterns between threads, but also hinders the modular verification of programs.

In this talk, we discuss an ongoing attempt to develop new logics for stateful reasoning in an unstructured concurrency setting. In particular, we propose a logic for fork/join concurrency that can reason modularly about forked threads and their interference. Our approach consists of bridging two previous works: we propose to combine the compositional expressiveness of fine-grained resources and FCSL with some lessons learnt while developing dependent type theories for stateful unstructured control.

The talk will introduce the C11 weak memory model that defines the semantics of concurrent C/C++ programs, and will answer two key questions regarding the model: (1) What high-level principles can programmers use to reason about their programs? (2) What source-to-source transformations can optimising compilers soundly perform?

I will present in this talk some insights about the formalization of mathematics, using the case study of a formal development of some elliptic curves theory in the coq proof assistant

The theory of elliptic curves is a subject where one finds diverse branches of mathematics, such as, complex analysis, algebraic geometry, representation theory and number theory. It has been an active field of study since the 19th century. Elliptic curves have been used to approach a wide range of problems such as the fast factorisation of integers and the search for congruent numbers. In the 20th century, they have regained interest because of their applications in cryptography, first suggested in 1985 independently by Neal Koblitz and Victor Miller. Elliptic curve theory remains a subject of active research because of its wide range of applications, as well as the rich mathematics behind it.

I will present a mapping from OCL (Object Constraint Language) to first-order logic. This mapping allows us to reason on UML models with OCL expressions and check satisfaction of them. Our translation considers the four-value characteristics of OCL and is significantly more comprehensive than previous works. Also, I will present a methodology for the analysis of ActionGUI models. ActionGUI models are composed of three UML based models aimed to describe the data, the security restrictions and the GUI behaviour. ActionGUI toolkit generates automatically code from UML, security and GUI models. The quality of the generated code depends on the quality of the source models. If the models do not specify the system intended behavior, one should not expect the generated system to do so either. Using the principles of the aforementioned result, we develop a methodology to analyze different kind of properties on ActionGUI models. They include checking consistency of the data model and analysis of invariant preservation on the GUI model. The methodology was implemented using SMT solvers and automatic theorem provers as back ends.