Parosh Aziz Abdulla
Uppsala University, Sweden
Quantum Circuit Verification: Challenges and Opportunities
Quantum technologies are progressing at an extraordinary pace and are poised to transform numerous sectors, both nationally and globally. Among these technologies, quantum computing stands out for its potential to revolutionize areas such as cryptography, optimization, and the simulation of quantum systems by offering dramatic speedups for specific classes of problems.
As quantum devices continue to evolve and become increasingly pervasive, ensuring their correctness is of paramount importance. This requires the development of rigorous methods and tools for analyzing and verifying their behavior. However, constructing such verification frameworks presents fundamental challenges. Quantum phenomena such as superposition and entanglement give rise to computational behaviors that differ profoundly from those of classical systems, resulting in inherently probabilistic models and exponentially large state spaces, even for relatively small quantum programs and circuits.
Addressing these challenges requires building on the extensive expertise of the formal methods community in classical program verification while incorporating recent advances in quantum computing and fostering close collaboration with the quantum computing community. A central challenge for the verification community is to design and implement novel verification frameworks that transfer the key strengths of classical verification—such as expressive specification languages, precise error detection, automation, and scalability—to the quantum domain.
Such advances will play a crucial role in enabling the dependable deployment of quantum technologies across a wide range of future applications.
Nadia Pisanti
University of Pisa, Italy
Alignments to and among degenerate strings
The notion of D strings and ED strings were investigated as an almost-linear version of pangenome graphs, that is, a collection of genomic sequences to be analyzed jointly or to be used as a reference. They can also be seen as a directed acyclic graph, whose nodes are labeled by strings.
I will describe notions of banded alignment and on-line matching to (E)D strings, and of matching statistics and similarity measures between (E)D strings.