publicações selecionadas
-
artigo académico
- Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications. Journal of Logical and Algebraic Methods in Programming. 2023
- 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
- Structural proof theory as rewriting. Computational Methods in Applied Sciences. 2006
- Type-based termination of recursive definitions. Mathematical Structures in Computer Science. 2004
- Constructor subtyping. Computational Methods in Applied Sciences. 1999
-
artigo de conferência
- A generalized program verification workflow based on loop elimination and SA form 2019
- A Generalized Approach to Verification Condition Generation 2018
- Permutability in proof terms for intuitionistic sequent calculus with cuts 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
- Constructor subtyping 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
-
documento
-
livro