Date: Tuesday, November 3 2026 – 13h00Place: A008Title: Relational Program Logics for Probabilistic and Quantum Computations The talk will present an overview of relational program logics for cryptography and differential privacy proofs. In the first part, I will emphasize how these programs logics have gradually evolve to achieve better expressiveness…
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: May 13, 2026Place: A008Chairs: Charlie Jacomme and Engel Lefaucheaux Tentative Schedule 10h00-12h: 12h00: pizzas in “salle club” (the room between the restaurant and the cafeteria) 13h00: coffee 13h30-15h35: Detailed program Colin Blake: Equational Reasoning for Qudit Circuits Abstract: Quantum programs are most often represented as quantum circuits: sequences of…
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…