Preuves Automatiques et Raisonnement sur des SpécIFicAtions Logiques
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.
January 2020 The Parsifal team has ended after more than 12 years. All members have moved to the new Partout team.
February 2019: The Parsifal team will end in December 2019 since Inria closes all teams after 12 years. Team members are in the process of proposing to Inria a new team named Partout and lead by Lutz Straßburger. All existing team members plan to join this team. The plan also calls for Partout to be a team within the LIX lab.
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.
