Date: Thursday, April 30 2026 – 14h00Place: B013 (Salle Bob)Title: Actor Programming and Verification: Specification-Guided Verification and Programming with LLM for Concurrent and Distributed Systems Actor model of computation (which will soon celebrate its 50th birthday) is introduced by Carl Hewitt at MIT’s AI Lab, and has panned over 30…
Date: Tuesday, May 5 2026 – 13h00Place: C005Title: Discriminations, Harassment and Unwell-being in Academia – Understand, React and Prevent Many studies, internationally or nationally, demonstrate that the academic world suffers from discriminations, harassment and unwell-being issues. It can be difficult to clearly acknowledge this and take actions against it, and…
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,…