LogSem Seminar talks in 2025

06-01-2025: Extending Iris with liveness reasoning

Speaker: Egor Namakonov, Aarhus University

Time: 13:00-14:00

Location: Nygaard-297

Abstract: Higher-order program logics like Iris have proven extremely expressive for the verification of safety properties. However, the same level of expressivity for liveness verification is yet to be achieved. The existing work in this area had to compromise either on higher-order reasoning, compositionality, verifying the whole development foundationally, or being language-agnostic. In this talk, I’ll give an overview of a few Iris developments that deal with liveness verification. Then, I’ll introduce Lawyer - our ongoing project aiming at achieving all of the aforementioned goals - and show how to use it to verify the termination of a simple concurrent program.

10-02-2025: Efficient simulation of High-Level Quantum Software

Speaker: Adam Husted Kjelstrøm, Aarhus University

Time: 13:00-15:00

Location: Ada-333

Abstract: Simulation is a natural way to investigate program behavior. Interestingly for the quantum setting, a single simulation is enough to determine equivalence between programs, making simulation algorithms powerful tools for verifying program correctness. Practical quantum computing is hampered by the high error rates of instructions. To improve practical performance, code minimizers are employed. In this setting, Simulators can be paired with heuristic search to equivalence check candidate smaller programs. To build such code minimizers, efficient simulation algorithms are crucial. In this presentation, I will introduce a simulator for high-level quantum software. Other simulators compile the user-provided code to a low-level representation before simulating, resulting in increased software size and an (exponential) blow-up in simulation time. By directly simulating high-level code, this overhead is avoided, resulting in efficient simulation of certain classes of quantum software.

It is natural to ask whether all quantum code can be efficiently simulated. Assuming SETH, I demonstrate how some quantum code can never be efficiently simulated. Specifically, access to even a single ADD instruction is enough to encode 3SAT.