BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260408T201932Z
UID:Seminar-verification-1334@lxserverA.csc.liv.ac.uk.csc.liv.ac.uk
ORGANIZER:CN=Patrick Totzke:MAILTO:totzke@liverpool.ac.uk
DTSTART:20260319T110000
DTEND:20260319T120000
SUMMARY:Verification Series
DESCRIPTION:Alexei Lisitsa: Quantum verification via tangles, quandles, and automated reasoning\n\n   In this talk, I will present our recent work on automating the verification of\n\n   quantum programs and circuits, building on a method proposed by Reutter and\n\n   Vicary (2019). In this framework, quantum circuits and programs are modelled as\n\n   tangles—informally, finite collections of strings or laces embedded and\n\n   entangled in three-dimensional space. Verification of program equivalence is\n\n   then reduced to the problem of tangle equivalence (isotopy), yielding a\n\n   conceptually simple and visually appealing approach.\n\n   Drawing on our earlier work on applying automated reasoning to computational\n\n   topology, particularly knot theory, we translate the resulting topological\n\n   problems into an algebraic setting. This is achieved using variants of\n\n   algebraic structures known as quandles. Automated reasoning tools (theorem\n\n   provers and model finders) are then employed to establish (non-)equivalence of\n\n   tangles, and hence of the corresponding quantum circuits.\n\n   I will conclude by highlighting several open questions and challenges, both in\n\n   the theoretical foundations of the approach and in its practical application to\n\n   quantum program verification.\n\n\n\n   Joint work with Andrew Fish.\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=1334
LOCATION:Ashton 208
END:VEVENT
END:VCALENDAR