Mechanizing Feng-Ying Quantum Hoare Logic in Coq for Formal Proofs of Programs with Quantum and Classical Variables EVALUATED

Detalhes: A lógica de Hoare é uma ferramenta poderosa para a verificação formal de software. Tem sido usado para provar a correção de muitos programas e protocolos, com varios tipos de programas, como determinísticos, não determinísticos, recursivos, paralelos, concorrentes ... e é um candidato adequado para asegurar a correção dos programas quânticos, como outras formas de teste e depuração tem um custo alto, ou não são confiáveis, no caso quântico. Neste tese vamos fazer uma curta introdução para computação quântica, Quantum Hoare Logic e seus fundamentos matemáticos que serão discutidos e comparados com alguns exemplos e aplicações do mundo real de algoritmos quânticos, e vamos implementar uma mecanização da lógica em Feng et al. usando o provador de teoremas Coq.

Discussão: dezembro 2, 2021, 16:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

AUTOR

Mustafa Samir Khalil (ist427068)

ORIENTADOR

João Fernando Peixoto Ferreira

Departamento de Engenharia Informática (DEI)

Professor Auxiliar