| Type-based termination of recursive definitions G Barthe, MJ Frade, E Giménez, L Pinto, T Uustalu Mathematical structures in computer science 14 (1), 97-141, 2004 | 145 | 2004 |
| Rigorous Software Development - An Introduction to Program Verification JB Almeida, MJ Frade, JS Pinto, SM de Sousa Springer, 2011 | 91 | 2011 |
| An overview of formal methods tools and techniques JB Almeida, MJ Frade, JS Pinto, S Melo de Sousa, JB Almeida, MJ Frade, ... Rigorous Software Development: An Introduction to Program Verification, 15-44, 2011 | 55 | 2011 |
| Verification conditions for source-level imperative programs MJ Frade, JS Pinto Computer Science Review 5 (3), 252-277, 2011 | 50 | 2011 |
| Constructor subtyping G Barthe, MJ Frade Programming Languages and Systems: 8th European Symposium on Programming …, 1999 | 37 | 1999 |
| Structural proof theory as rewriting JE Santo, MJ Frade, L Pinto Term Rewriting and Applications: 17th International Conference, RTA 2006 …, 2006 | 17 | 2006 |
| Type-Based Termination of Recursive Definitions and Constructor Subtyping in Typed Lambda Calculi MJ Frade | 11 | 2003 |
| Verification conditions for single-assignment programs D da Cruz, MJ Frade, JS Pinto Proceedings of the 27th Annual ACM Symposium on Applied Computing, 1264-1270, 2012 | 10 | 2012 |
| Formalizing single-assignment program verification: An adaptation-complete approach C Belo Lourenço, MJ Frade, J Sousa Pinto Programming Languages and Systems: 25th European Symposium on Programming …, 2016 | 8 | 2016 |
| Foundational certification of data-flow analyses MJ Frade, A Saabas, T Uustalu First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software …, 2007 | 7 | 2007 |
| A bounded model checker for SPARK programs CB Lourenço, MJ Frade, JS Pinto International Symposium on Automated Technology for Verification and …, 2014 | 6 | 2014 |
| Permutability in proof terms for intuitionistic sequent calculus with cuts J Espírito Santo, MJ Frade, LF Pinto Schloss Dagstuhl–Leibniz-Zentrum für Informatik GmbH, 2018 | 5 | 2018 |
| A generalized program verification workflow based on loop elimination and SA form CB Lourenço, MJ Frade, JS Pinto 2019 IEEE/ACM 7th International Conference on Formal Methods in Software …, 2019 | 4 | 2019 |
| Bidirectional data-flow analyses, type-systematically MJ Frade, A Saabas, T Uustalu Proceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and …, 2009 | 4 | 2009 |
| Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications JE Santo, MJ Frade, L Pinto Journal of Logical and Algebraic Methods in Programming 131, 100830, 2023 | 3 | 2023 |
| A generalized approach to verification condition generation CB Lourenço, MJ Frade, S Nakajima, JS Pinto 2018 IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC …, 2018 | 3 | 2018 |
| TreeCycle: a Sonar plugin for design quality assessment of Java programs JM Veiga, MJ Frade Techn. Report CROSS-10.07-1, 2010 | 3 | 2010 |
| Calculus of Inductive Constructions MJ Frade | 2 | 2008 |
| A verified VCGen based on dynamic logic: An exercise in meta-verification with Why3 MJ Frade, JS Pinto Journal of Logical and Algebraic Methods in Programming 133, 100871, 2023 | 1 | 2023 |
| A Tutorial on Verification Conditions Using Single-Assignment Form CB Lourenço, MJ Frade, JS Pinto unpublished draft available from http://haslab. uminho. pt/jsp), University …, 2015 | 1 | 2015 |
