Consortium as a whole

The participants to the consortium group together the minimal set of skills, know how and resources capable of achieving the project objectives. The project lies at the intersection between complexity, formal checking and compilers, requiring not only experts of the three fields, but also people with some knowledge and sensibility towards all the different topics.

The main research field of UNIBO is currently on tools and techniques for the automation of formal reasoning, and especially on the development of the new Interactive Theorem Prover Matita and its applications to correctness proofs for critical software applications. The group has direct experience on the formalization of micro-controllers in Matita, as testified by an executable specification for all models of Freescale 8bit micro-controllers available at the address� The formalization captures all ALU families (Families HC05/HC08/RS08/HCS08) and all kind of memories that can be installed (RAM, ROM, Flash). The formalization comprise the computational cost of every machine operation, allowing to reason at the level of granularity of single clock cycles. An OCaml emulator running at reasonable speed has also been automatically extracted from the executable specification. In addition, the UNIBO site has past didactical and experimental experience in compiler construction, and good knowledge of complexity theory. In particular, Andrea Asperti held the chair in Programming Languages and Compilers in the period 1992-2000, writing scientific and didactical monographs on the topics,^6^? and is currently teaching Computability and Complexity Theory.

The present research focus of UPD is mostly on complexity aspects, and resource control for real time systems, but they are expert in compiler construction, and comprise members with good experience in the use of interactive provers. In particular, Roberto Amadio is currently teaching a course on Syntax Analysis and Compilers at the University of Paris Diderot and he recently coordinated the National Project�amadio/Criss/criss.htmlCriss, comprising the development of a small�amadio/Criss/shape-analysis.htmlcompiler for a first order functional language, producing bytecode annotated with relevant complexity information using shape analysis. This compiler was programmed in OCaml.

Finally, UEDIN offers much experience in the theory and implementation of programming languages, with particular emphasis on the formal engineering of their metatheory. Randy Pollack is the author of LEGO, a well known Interactive Prover of the nineties (no longer maintained) that was used by many students and researchers. Prior to that, Pollack had been an industrial software engineer specializing in real-time systems. He is currently working in the Mobility and Security Group at UEDIN, which has participated in 2 recent EU projects on formal certification of resource properties.^7^? Pollack was also on the steering committee of the recently completed EU Coordination Action In addition, UEDIN has significant research groups in areas of complexity and compilers.

All the partners have previously worked, alone or together, in European projects of different nature and sizes, including RTD projects. The above mentioned projects have successfully completed, demonstrating the capabilities of the CerCo? partners of carrying out projects of European dimension, as well as their positive attitude to collaborative work. In many cases, the partners CerCo? Consortium have acted as project coordinators; as such, they are well aware of execution and management policies of EU-funded projects.


Subcontractors will only be used for production of Certificates of Financial Statements, as required by FP7 rules. Other subcontracting has not resulted to be necessary since all competences required for carrying out the action are represented within the consortium.

Last modified 7 years ago Last modified on Jun 15, 2010, 1:03:44 PM