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: May 6, 2025Place: A008Chairs: Charlie Jacomme and Engel Lefaucheaux Each presentation will last a total of maximum 30 minutes (20 minutes talks + 10 minutes of question/setting up). We encourage all talks to be given in English. Tentative schedule 9h30 – 10h30: Florian Moser, Joannes Guichon 10h30 – 10h45:…
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: Monday, February 19th 2024 – 13h00Place: B013 (Bob)Title: Communicating automata and k-synchronizability Distributed systems are ubiquitous and their implementation is complex and error-prone. In order to check for errors, they can be modeled as systems of communicating automata, where each automaton represents the behavior of an element of the…
