Date: May 6, 2025
Place: A008
Chairs: 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: Coffee break 1
- 10h45 – 12h15: Colin Blake, Sarah Dépernet, Léo Louistisserand
- 12h15 – 14h00: pizzas!
- 14h00 – 15h30: Benjamin Testart, Thomas Vinet, Kathleen Barsse
- 15h30 – 15h45: Coffee break 2
- 16h00 – 17h30: Quentin Jacqmin, Benjamin Izart, Jad Issa
Detailed program
Joannes Guichon – “B2B debt netting : temporal considerations”
Abstract : “In the business-to-business (B2B) landscape, the temporal dynamics of invoice settlements are critical to the financial health of companies. Recurrent late payments create a network of interlocking debts, where each firm is simultaneously a creditor and a debtor. This situation can provoke liquidity crises and systemic risk. A method to reduce such risk is the integral netting mechanism, in which selected invoices are fully settled by injecting minimal external liquidity at well-chosen points in the network. Methods have been proposed for B2B transactions in a fixed time period. A central question is: how to adapt such netting to a real-world scenario in which invoices arrive continuously over time ?”
Florian Moser – “Internet Voting without trusting the end-user’s device – and a formal proof of security”
Abstract: When performing elections over the internet, similar guarantees as in regular elections must be safeguarded: An internet voting system must guarantee privacy (hence the individual voter’s choice remains private) and correctness (hence all votes are counted as cast). We present a mechanism that is able to achieves these guarantees without trusting the end-users device. Further, we present a formal proof over the system’s privacy and correctness.
Colin Blake – “Escape the Matrix: Graphical Reasoning and Minimal Axioms for Quantum Circuits”
Abstract: Quantum circuits are commonly represented using matrices, but this approach becomes unwieldy for complex systems. In this talk, I will present a graphical methodology that utilizes equational rules to rewrite circuits, offering a more intuitive and structured framework. We will discuss the criteria for such a system to be sound, complete, and minimal, and explore the significance of these properties. Subsequently, I will introduce new minimal equational theories for various classes of quantum circuits, each with distinct expressive capabilities. These minimality results are significant because they simplify the equational theory by eliminating redundant rules, making it more practical for applications like circuit optimization and verification.
No prior background in quantum computing is required; the emphasis will be on the foundational formal concepts.
Benjamin Testart – “Enumeration of pattern-avoiding inversion sequences”
Abstract: An inversion sequence is a finite sequence of integers (s_1, …, s_n) such that each term s_i satisfies 0 ≤ s_i < i. In this talk, we will give an overview of various constructions of such sequences. These constructions allow us to obtain efficient counting formulas for the number of inversion sequences (of any given length) satisfying pattern-avoidance constraints. There will be a focus on the generating tree approach, which consists in identifying combinatorial objects (in this case, inversion sequences) with the nodes of a labelled rooted tree that is described by a rewriting rule.
Léo Louistisserand – “Vote&Check: Secure Postal Voting with Reduced Trust Assumptions”
Postal voting is a frequently used alternative to on-site voting. Traditionally, its security relies on organizational measures, and voters have to trust many entities. In the recent years, several schemes have been proposed to add verifiability properties to postal voting, while preserving vote privacy. Postal voting comes with specific constraints. We conduct a systematic analysis of this setting and we identify a list of generic attacks, highlighting that some attacks seem unavoidable. This study is applied to existing systems of the literature. We then propose Vote&Check, a postal voting protocol which provides a high level of security, with a reduced number of authorities. Furthermore, it requires only basic cryptographic primitives, namely hash functions and signatures. The security properties are proven in a symbolic model, with the help of the ProVerif tool.
Thomas Vinet – “A hybrid and reversible quantum language”
We present a typed quantum reversible language that features both classical and quantum data, a minimal but expandable set of types, quantum superpositions and recursion. We introduce a syntax to define reversible terms using a set of clauses and pattern-matching; and while verifying reversibility is undecidable in most cases, we give a decidable predicate to check and find the inverse for a significant subset of reversible terms. Finally, we discuss about viewing our language as a term-rewriting system in order to analyze the resources used by a program.
Jad Issa – “Statically evaluating termination and estimating ressources of quantum programs”
Quantum computation is rapidly growing in interest. With recent advances in quantum
hardware, it is becoming more and more evident that the next obstacle in the way of practical
quantum computing is in understanding the behavior of quantum programs. However, as
quantum computers are still in their infancy, and are not expected to become available in
cheap and easy-to-access consumer products for a while, if ever, testing and benchmarking
quantum programs on real hardware is not a viable option for the average programmer. Instead,
we propose methods to statically analyze hybrid programs (programs that mix classical and
quantum code) in order to prove their termination, when possible, and estimate their resource
usage or complexities. Our approach is based on a form of classical symbolic execution of the
program into a representation known as a path-sum. Our essential contribution is enriching this
path-sum formalism so that it can handle questions of termination and resource estimation. We
illustrate our approach on a simple program known as a ‘coin-toss’, and highlight the properties
we have proved about it and its shortcomings. Finally, we discuss the continuation of this work
in progress, and the longer-term goals and directions of research that spawn from it.
Sara Depernet – “Opacity in timed automata”
Timed automata are an extension of finite automata enhanced by real-valued clocks which measure the time elapsed in the states of the system. They are used to model real-time systems. I am interested in a security property called opacity, which corresponds to resistance against side channel attacks in cybersecurity. These attacks consist in deducing private data by using external observations of the system, such as total execution times. A timed automaton is opaque whenever no such leak is possible. This property is strongly related to formal language inclusion problems. I study the complexity of checking opacity properties on timed automata, and on some of their subclasses.
WIP
