Date: Tuesday, February 20th 2025 – 13h00Place: A008Title: The Lisa Proof Assistant & Efficient and Predictable Tools with Orthologic-Based Reasoning In this talk, I will present my research efforts in improving and developing automated reasoning tools. First, I will present Lisa, a proof assistant based on Set Theory that I…
Date: Tuesday, February 4th 2025 – 13h00Place: A008Title: The Squirrel Prover The Squirrel Prover is a proof assistant dedicated to cryptographic protocols. It relies on a higher-order logic following the computationally complete symbolic attacker approach. It thus provides guarantees in the computational model. In this talk, we will introduce the…
Date: Tuesday, Janary 7th 2025 – 13h00Place: A008Title: Sup, Sum, and Scalars: In Linear Logic and in Non-Linear Logic In [1], we introduced a new connective, called “sup”, to intuitionistic propositional logic to model information erasure, non-reversibility, and non-determinism, as observed in quantum measurement, among other contexts. This connective features…
Date: Tuesday, March 4th 2025 – 13h00Place: A008Title: A scalable framework for backward bounded static symbolic executionMany programs (e.g. malware) hide their behavior by using obfuscations such as opaque predicates.Automatic methods have been developed to detect such obfuscations. In this presentation, we will focus on static symbolic backward bounded execution,…
Date: Tuesday, December 3rd 2024 – 13h00Place: A008Title: The Automation of Mathematics in Practice This presentation provides an overview of automated systems actively used in proving mathematical theorems, focusing on the practical successes achieved by SAT solvers, first-order theorem provers, and interactive theorem provers.Additionally, we present our progress towards improving…
Date: Tuesday, November 3rd 2024 – 13h00Place: A008Title: SC-TPTP : étendre le format TPTP pour les preuves basées sur les séquents
Date: Thursday, March 14th 2024 – 13h00Place: visioTitle: Conception d’un prouveur automatique basé sur les tableaux analytiques et production de preuves vérifiables La déduction automatique est l’utilisation de programmes informatique afin d’automatiquement prouver des théorèmes mathématiques. Elle trouve son intérêt dans la détection de bogues au sein de systèmes critiques…
Date: Friday, June 23rd 2023 – 14h00Place: C103Title: The TPTP World – Infrastructure for Automated Reasoning The TPTP World is a well known and established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems for classical logics. The data, standards, and services provided by the TPTP World…
Title : Computable Functions in Anonymous NetworksDate: Tuesday, May 23rd 2023 – 14h00Place: C103 Abstract: In this talk, we present several computability results in anonymous networks with broadcast communications. First, we recall the characterization, given by Boldi and Vigna, of the computable functions when agents have no information on their outgoing neighborhoods. Then we…
Title : Guaranteed properties of dynamical systems under perturbations.Date: Wednesday, May 3rd, 2023 – 14h00.Place: B013 Abstract : Since dynamical systems has a major impact on human development, especially critical systems that can put human lives at risk if something goes wrong. Hence, the need of studying the behavior of these systems in order to…
