Formal Models of Computing and Their Applications

Look here for detailed project content (postscript)

Concurrent Models and Applications

Because of the growing importance of networks and distributed systems there is a need for formal programming models based on concurrency theory. Current work done in our groups in this direction heads toward modeling of mobility as started in the pi-calculus, towards unification of functional and concurrent programming, and towards type theory extensions to concurrent processes.

The Meije team develops the blue calculus, while keeping up with exploration of properties around the pi-calculus. The Para team develops the join-calcul. Huimin Lin's team at the Software Institute of the Chinese Academy of Sciences in Beijing studies methods and tools for process algebras with data and channel passing. Fu Yuxi at Shanghai JiaoTong University is developing a calculus where concurrent processes communicate with each other by exchange channel names.

Abstract Models of Sequential and Parallel Computation

Types and Proof Theory

Automated Reasoning and Program Verification

Zhang Jian from the institute of software applies finite model generation technique to the analysis and verification of computer programs. He is experimenting on solve predicate equation systems using the tools he originally developed for automated reasoning. These equation systems come naturally from model checking or equivalence checking in the area of formal verification of computer hardware and/or software.

Coordinators

Gérard Boudol 
Meije project 
INRIA Sophia-Antipolis		 Huimin Lin lhm@ox.ios.ac.cn 
Institute of Software, Beijing 
Chinese Academy of Sciences
 

Other participants

Robert de Simone
Last modified: Fri Dec 5 11:03:44 MET