Proposta de dissertação do MEI Título: Formally Verified Bug-free Implementations of (Logical) Algorithms Proponente(s): António Ravara e Mário Pereira Créditos: 42 ECTS Área científica: Software Construction and Analysis Início preferencial: 1º Semestre URL: http://ctp.di.fct.unl.pt/FACTOR/ Já estão em curso trabalhos preliminares executados pelo alunos: Breve descrição: Soundness is presently a major challenge for programmers - the societal tolerance to software bugs and hacker infiltrations is decreasing, with prominent cases making news daily. There are however effective methodologies and tools to ensure safe and reliable programs, as witnessed by successful industrial cases. The vast majority of developers have little training in developing bug-free and hacker-proofed program. Moreover, most companies lack the know-how and practices to deal with these urgent software soundness challenges. The aim of this project is to develop formally verified functional implementations of classical logical algorithms like the Horn satisfiability. Concretely, the objective is twofold: - the functional implementation of classical logical algorithms as showcases of clean and clear code close to specifications; - the development of correctness proofs of the implementations as showcases of the feasibility and usability of machine-checked program proof systems. Observações: The project is part of a larger one running this academic year in the Department, funded by the Tezos Foundation (on Blockchain technology). The selected student will be supported by a grant of circa €850 throughout the thesis development period.