Date: Thursday, March 3 2026 – 13h00Place: C005Title: Deductive and Collaborative Verification of Implementations with Frama-C While ensuring the correctness of an implementation based on a formal functional specification provides extremely strong guarantees, it can be very expensive to achieve. In practice, a combination of formal methods is commonly employed…
Date: Thursday, February 5 2026 – 13h00Place: A008Title: Thin spans and their modelling of rigid intersection types Thins spans were recently introduced as a quantitative, or proof-relevant, modelof programming languages based on spans of groupoids. As a model of linearlogic, they can be seen as an extension of the relational…
Date: Monday, January 12 2026 – 13h00Place: A008Title: Random Variate Generation with Formal Guarantees Standard software libraries for random variate generation are based on “Real-RAM” algorithms, which assume infinite precision. The “Real-RAM” assumption, however, is unrealistic as any software implementation must use only finite precision. As a result, existing libraries…
Date: Tuesday, December 9 2025 – 13h00Place: A008Title: Hardware-Software Co-Designs for Microarchitectural Security Microarchitectural optimizations, such as caches and speculative out-of-order execution, are essential for achieving high system performance. However, these same mechanisms also open the door to attacks that can undermine software-enforced security policies. The current gold standard for…
Date: Thursday, November 13 2025 – 13h00Place: A008Title: Breaking verifiability and vote privacy in CHVote CHVote is one of the two main electronic voting systems developed in the context of political elections in Switzerland, where the regulation requires a specific setting and specific trust assumptions. We show that actually, CHVote…
Date: Thursday, October 16 2025 – 13h00Place: A008Title: Formalizing Splitting in Isabelle/HOL In this talk, I will present a formalization in Isabelle/HOL of a framework for splitting, a theorem proving technique that extends saturation-based calculi with branching abilities. The framework preserves the completeness of the original calculus. This work focuse…
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…