ABSTRACT. It is shown how the operators in the "graph model" for λ-calculus (which can function as a programming language for Recursive Function Theory) can be expanded to allow for "random combinators". The result then is a model for a basic language for random algorithms. The author has lectured about this model over the last year, but he wants to appeal for APPLICATIONS. The details of the model are so easy and so fundamental, the idea has to be useful.

ABSTRACT. Contracts are specifications of systems in which the respective roles of component vs. environment are made explicit. Contracts come with a rich algebra, including in particular a game oriented notion of refinement, a conjunction for fusing different aspects of the specification, and a parallel composition supporting independent development of sub-systems. Contracts can address the functional behavior of embedded systems, as well as other aspects of it, such as timing, resources, etc. Several frameworks have been proposed in the last decade offering -- sometimes in part -- such features, e.g., de Alfaro-Henzinger Interface Automata, K. Larsen's Modal Automata, and Benveniste et al. Assume/Guarantee contracts. Extensions to deal with time, resources, and probability, have been proposed. In this talk we develop a generic framework of contracts (we call it a meta-theory of contracts) that can be instantiated to any of the known concrete frameworks. This generic framework highlights the essence of this concept and allows equipping it with testing and abstraction apparatuses. We then illustrate through an example the use of Modal Interfaces, a specialization of the former, for Requirements Engineering, a demanding area too often dismissed by the community of formal verification. This is collective work by B. Caillaud, D. Nickovic, R. Passerone, J-B. Raclet, Ph. Reinkemeier, A. Sangiovanni-Vincentelli, W. Damm, T. Henzinger, and K.G. Larsen.

ABSTRACT. Diagrams (aka. graphs, charts, nets) are widely used to describe the behaviour of physical systems, including computer clusters under control of a program. Their behaviour is modelled as a non-metric plane geometry, with coordinates representing space and time. Points represent events, arrows represent messages and state, and lines represent objects and threads. The geometry is governed by a simple set of axioms, which are yet powerful enough to prove correctness of geometric constructions. Perhaps they extend to more general programs written in a concurrent programming language.

ABSTRACT. Probabilistic model checking is an automated method for verifying probabilistic models against temporal logic specifications. This lecture will give an overview of the role of that probabilistic model checking, and particularly the probabilistic model checker PRISM can play when modelling and analysing molecular networks at the nanoscale. In particular, the lecture will discuss how the technique has been used to advance scientific discovery through ‘in silico’ experiments for molecular signalling networks; debugging of DNA circuits; and performance and reliability analysis for molecular walkers.

http://www.prismmodelchecker.org ; http://www.veriware.org/dna.php 

ABSTRACT. TBA

ABSTRACT. Formal verification aims to improve the quality of hardware and software by detecting errors before they do harm. At the basis of formal verification lies the logical notion of correctness, which purports to capture whether or not a circuit or program behaves as desired. We suggest that the boolean partition into correct and incorrect systems falls short of the practical need to assess the behavior of hardware and software in a more nuanced fashion against multiple criteria. We propose quantitative fitness measures for reactive models of concurrent systems, specifically for measuring function, performance, and robustness. The theory supports quantitative generalizations of the paradigms that have been success stories in qualitative reactive modeling, such as compositionality, property-preserving abstraction, model checking, and synthesis.

ABSTRACT. TBA

ABSTRACT. Cancer is a highly complex aberrant cellular state where mutations impact a multitude of signalling pathways operating in different cell types. In recent years it has become apparent that in order to understand and fight cancer, it must be viewed as a system, rather than as a set of cellular activities. This mind shift calls for new techniques that will allow us to investigate cancer as a holistic system. In this talk, I will discuss some of the progress made towards achieving such a system-level understanding by viewing cancer as a reactive system and using computer modelling and formal verification. I will concentrate on our recent attempts to better understand cancer through the following four examples: 1) drug target optimization for Chronic Myeloid Leukaemia using an intuitive interface called BioModelAnalyzer, which allows to prove stabilization of biological systems; 2) dynamic hybrid model of brain tumour development using F#; 3) state-based models of cancer signalling crosstalk and their analysis using model-checking; and 4) synthesis of biological programs from mutation experiments. Looking forward, inspired by David Harel’s Grand Challenge proposed a decade ago, I will propose a smaller grand challenge for computing and biology that could shed new light on our ability to control cell fates during development and disease and potentially change the way we treat cancer in the future.

ABSTRACT. TBA

ABSTRACT. TBA

ABSTRACT. Synthesis is the automated construction of a system from its specification. In standard temporal-synthesis algorithms, it is assumed the system is constructed from scratch. This, of course, rarely happens in real life. In real life, almost every non-trivial system, either in hardware or in software, relies heavily on using libraries of reusable components. Furthermore, other contexts, such as web-service orchestration and choreography, can also be modeled as synthesis of a system from a library of components. In this talk we describe and study the problem of compositional temporal synthesis, in which we synthesize systems from libraries of reusable components. We define two notions of composition: data-flow composition, which we show is undecidable, and control-flow composition, which we show is decidable. We then explore a variation of control-flow compositional synthesis, in which we construct reliable systems from libraries of unreliable components. Joint work with Yoad Lustig and Sumit Nain.