publicações selecionadas
-
artigo académico
- Verification conditions for single-assignment programs. Proceedings of the ACM Symposium on Applied Computing. 2012
- Bidirectional data-flow analyses, type-systematically. Proceedings of the 2009 ACM SIGPLAN Symposium on Partial Evaluation and Program Manipulation, PEPM'09. 2009
- Foundational certification of data-flow analyses. First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE '07. 2007
-
artigo de conferência
- A generalized program verification workflow based on loop elimination and SA form. FME Workshop on Formal Methods in Software Engineering. 2019
- A generalized approach to verification condition generation. Proceedings International Computer Software and Applications Conference. 2018
- Permutability in proof terms for intuitionistic sequent calculus with cuts. Leibniz International Proceedings in Informatics, LIPIcs. 2018
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach. Computational Methods in Applied Sciences. 2016
- A Bounded Model Checker for SPARK Programs. Computational Methods in Applied Sciences. 2014
- Structural proof theory as rewriting. Computational Methods in Applied Sciences. 2006
- Constructor subtyping. Computational Methods in Applied Sciences. 1999
-
artigo de revista
- A verified VCGen based on dynamic logic: An exercise in meta-verification with Why3. Journal of Logical and Algebraic Methods in Programming. 2023
- Verification conditions for source-level imperative programs. Computer Science Review. 2011
- Type-based termination of recursive definitions. Mathematical Structures in Computer Science. 2004
-
documento
- Experimenting with predicate abstraction 2013
- SPARK-BMC: checking SPARK code for bugs 2013
- Guiões das aulas práticas laboratoriais sobre o sistema COQ 1998
- Introdução ao sistema COQ de assistência à prova 1998
- Sebenta prática de elementos lógicos da programação I : guiões das sessões laboratoriais no sistema Isabelle 1998
- Comunicação, concorrência e processos 1995
- Navegar é preciso... 1994
-
relatório
-
teses