ANR has selected the project ICSPA (Interoperable and Confident Set-based Proof Assistants) under the framework “appel à projets générique 2020”.
- DURATION: 48 months
- PARTENERS: Samovar Paris (leader), CLEARSY, INRIA Nancy, INRIA Saclay, IRIT Toulouse, LRIMM Montpelier
ICSPA focuses on the set-based specification formalisms B, Event-B, and TLA+ that have been adopted for industrial development projects, for applications where correctness is critical. It aims at reinforcing the confidence in proofs carried out mechanically using them.
Our project also aims at designing and implementing an exchange framework, through which those three systems can share their proofs and theories, making them effectively interoperable.