Preuves Automatiques et Raisonnement sur des SpécIFicAtions Logiques
The Parsifal team works on foundational aspects of proof theory as well as on the design and implementation of systems that exploit that foundational work. Recently prototyped systems support logic programming, model checking, and automated reasoning. These systems are used to study a wide range of computational logic issues, including program correctness, security, concurrency, and operational semantic specifications and their formalized meta-theory.
Parsifal has been a team within LIX since September 2003 and an INRIA project-team (“Équipe-projet INRIA” or EPI) since October 2007. During the INRIA Evaluation Seminar in Paris on 23 March 2011, the Parsifal EPI presented an overview of its work during 2007-2011.