- Pedro Barroso, Mário Pereira and António Ravara: Correct Functional Conversion to Conjunctive Normal Form [pdf]. In Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square), co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020)
- Pedro Barroso: Formally Verified Bug-free Implementations of (Logical) Algorithms [uri]. Masters Thesis in Computer Science and Engeeniring, NOVA School of Science and Technology, Portugal. January 2020.