Brisbane. Photo by Martin on Unsplash
| Time | Content | |
|---|---|---|
| 10:00 - 10:45 | Opening | Kazuhiro Ogata. An overview of FAVPQC achievements. [slides] |
| 10:45 - 11:15 | Break | |
| 11:15 - 12:15 | Session 1: Formal specification and verification of post-quantum cryptographic protocols | |
| 11:15 - 11:45 | Víctor García, Santiago Escobar and Kazuhiro Ogata. Formal specification of the post-quantum signature scheme FALCON in Maude. [paper] [slides] | |
| 11:45 - 12:15 | Duong Dinh Tran, Kazuhiro Ogata and Santiago Escobar. A formal analysis of OpenPGP's post-quantum public-key algorithm extension. [paper] [slides] | |
| 12:15 - 14:15 | Lunch | |
| 14:15 - 15:15 | Session 2: Formal verification of quantum programs/circuits | |
| 14:15 - 14:45 | Canh Minh Do, Tsubasa Takagi and Kazuhiro Ogata. Automated Quantum Program Verification in Probabilistic Dynamic Quantum Logic. [paper] [slides] | |
| 14:45 - 15:15 | Canh Minh Do and Kazuhiro Ogata. Symbolic Model Checking Quantum Circuits With Density Operators in Maude. [paper] [slides] | |
| 15:15 - 15:45 | Break | |
| 15:45 - 16:45 | Session 3: Foundation of quantum programs/circuits from verification | |
| 15:45 - 16:15 | Tsubasa Takagi, Canh Minh Do and Kazuhiro Ogata. Reachability Analysis of the Equivalence of Two Terms in Free Orthomodular Lattices. [paper] [slides] | |
| 16:15 - 16:45 | Canh Minh Do and Kazuhiro Ogata. Theoretical Foundation for Equivalence Checking of Quantum Circuits. [paper] [slides] | |
| 16:45 - 17:00 | Closing | |