Getting a Grant
IPM Formal Methods Day
10 January 2016
The registration fee must be paid to the following account:
(You can pay from any branch of Melli Bank in Iran.)
Institute for Research in Fundamental Sciences
Niavaran Street, Tehran
December 20, 2015
January 1, 2016
The goal of this one day event is to bring together internationally leading computer scientists to present the field of “formal methods” and their applications in other areas of science and engineering, to a wider academic community. The invited talks will cover a range of topics from foundations to the application of formal methods in biological science and quantum computing.
All researchers interested to find out about formal methods and their applications are invited to attend this event and exchange ideas with our invited world renowned experts in the field. This event precedes immediately before
The First IPM Advanced School on Computing.
Joseph Sifakis, EPFL & Verimag/CNRS [Turing Award winner of 2007]
Rigorous system design
Today, the development costs of high confidence systems explode with their size. We are far away from the solution of the so called, software crisis. In fact, the latter hides another much bigger: the system crisis.
In my talk I will discuss rigorous system design as a formal and accountable process leading from requirements to correct-by-construction implementations. I will also discuss current limitations of the state of the art and advocate a coherent scientific foundation for system design based on four principles: 1) separation of concerns; 2) component-based construction; 3) semantic coherency; 4) correctness-by-construction. The combined application of these principles allows the definition of a methodology clearly identifying where human intervention and ingenuity are needed to resolve design choices, as well as activities that can be supported by tools to automate tedious and error-prone tasks.
The presented view for rigorous system design has been amply implemented in the BIP (Behavior, Interaction, Priority) component framework and substantiated by numerous experimental results showing both its relevance and feasibility.
I will conclude with a discussion advocating a system-centric vision for computing, and a deeper interaction and cross-fertilization with other more mature scientific disciplines.
Jan Rutten, Radboud University Nijmegen/CWI
The method of coalgebra: an informal introduction
Since the early nineties, coalgebra has become an active area of research in which one tries to understand all kinds of infinite data types, automata, transition systems and dynamical systems from a unifying perspective. The focus of coalgebra is on observable behaviour and one uses coinduction as a central methodology, both for behavioural specifications and to prove behavioural equivalences. These days, one uses coalgebraic techniques in a wide variety of areas, ranging from automata theory to software engineering to economy. In this lecture, we shall give a non-technical overview of the main ingredients of the coalgebraic method.
Wan Fokkink, Vrije Universiteit Amsterdam, Netherlands
What can formal methods bring to systems biology?
Operational modelling approaches from the formal methods community can be applied fruitfully within the systems biology domain. The results can be complementary to the traditional mathematical descriptive modelling approaches used in systems biology. We discuss one example: a Petri net analysis of C. elegans vulval development.
Elham Kashefi, The University of Edinburgh
Verification of quantum computing
Over the next five to ten years we will see a state of flux as quantum technologies become part of the mainstream computing landscape. These devices will not be universal in terms of having a simple programming model nor will they be easily applicable to all problems. Adopting and applying such a highly variable and novel technology has an acute verification problem: On the one hand, since classical computations cannot scale up to the computational power of quantum mechanics, verifying the correctness of a quantum-mediated computation is challenging; on the other hand, the underlying quantum structure resists classical certification analysis. In this talk we present a new approach for testing the correctness of any delegated quantum computing based on the ability to compute with encrypted data, while hiding the underlying function.
Marjan Sirjani, Reykjavík University, Iceland
On-time actors in doubt
The good old days of computation when we abstracted away time and uncertainty are passed. In this new era of Cyber-Physical systems, we have to address timeliness and probability as main features in our models. To explore the design space, and to analyse safety and performance of models efficiently and effectively we need usable and analysable models. Probabilistic Timed Rebeca is introduced to enable model driven development and bridge the gap between formal methods and software engineering. The language is actor-based and therefore is natural for building distributed, asynchronous, and event-based systems. Model checking and simulation tools are developed to support formal verification and performance evaluation. In this talk I will explain Rebeca together with the timed and probabilistic extensions of it, and show how it can be used in model driven development using a Network on Chip example.
Vincent Danos, The University of Edinburgh
The macroeconomics of the cell
We develop coarse-grained models of the cell; explain the inherent resource allocation problem which the cell has to solve; and derive from a simple model constraints on the cell's steady state chemical composition which have been empirically identified as the "growth laws".
Back to top
Farhad Arbab, Leiden University/CWI
Ebrahim Ardeshir-Larijani, IPM
Back to top
Copyright 2000, All rights reserved.
School of Computer Science, Institute for Research in Fundamental Sciences (IPM)
Please send your comments or questions to