9 papers
An MSO Framework for Weak-Memory Verification and Robustness
Giovanna Kobus Conrado, Andreas Pavlogiannis
Memory models are formal specifications of concurrent-program executions, accounting for weak behaviors introduced by compiler and architectural optimizations. The increase of thei…
Efficient Simulation of High-Level Quantum Gates
Adam Husted Kjelstrøm, Andreas Pavlogiannis, Jaco van de Pol
Quantum circuit simulation is paramount to the verification and optimization of quantum algorithms, and considerable research efforts have been made towards efficient simulators. W…
On the Decidability of Verification under Release/Acquire
Giovanna Kobus Conrado, Andreas Pavlogiannis
The verification of concurrent programs under weak-memory models is a burgeoning effort, owing to the increasing adoption of weak memory in concurrent software and hardware. Releas…
Fast Atomicity Monitoring
Hünkar Can Tun, Yifan Dong, Andreas Pavlogiannis
Atomicity is a fundamental abstraction in concurrency, specifying that program behavior can be understood by considering specific code blocks executing atomically. However, atomici…
Exact Quantum Circuit Optimization is co-NQP-hard
Adam Husted Kjelstrøm, Andreas Pavlogiannis, Jaco van de Pol
As quantum computing resources remain scarce and error rates high, minimizing the resource consumption of quantum circuits is essential for achieving practical quantum advantage. H…
The Complexity of Testing Message-Passing Concurrency
Zheng Shi, Lasse Møldrup, Umang Mathur +1
A key computational question underpinning the automated testing and verification of concurrent programs is the consistency question - given a partial execution history, can it be c…