Date: Tuesday, March 18, 2025 – 13h00Place: B013 (Bob)Title: On reachability games played on graphs Nowadays computer systems are more and more involved in our everyday life. These systems become increasingly complex and interact either together or with humans. Moreover, in some situations bugs may have dramatic consequences. Thus, given…
Date: Tuesday, April 1st 2025 – 13h00Place: A008Title: Infinite Algebraic Proofs Lors du séminaire du département du 7 janvier, Alejandro a montré comment étendre le fragment multiplicatif-additif de la logique linéaire intuitionniste au cas quantique.En particulier, il a montré comment représenter, à travers un système de preuve et par Curry-Howard,…
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…
