Publications
V. C. Miraldo, M. J. Frade, C.Lourenço, J. S. Pinto Experimenting with Predicate Abstraction. Proceedings of INForum'13 –- Simpósio de Informática (SOFTPT track). (, Eds.). Universidade de Évora, 2013.
SPARK-BMC: Checking SPARK Code for Bugs (Comunicação). Proceedings of INForum'13 –- Simpósio de Informática (SETR track). (, Eds.). Universidade de Évora, 2013.
– D. Cruz, M. J. Frade, J. S. Pinto. Verification Conditions for Single-assignment Programs. In Software Verification and Testing 2012, (a track of the ACM 27th Symposium On Applied Computing, SAC 2012), March 26-30, 2012, Riva de Garcia (Trento), Italy.
– M. J. Frade, J. S. Pinto. Verification Conditions for Source-level Imperative Programs. In Computer Science Review, Volume 5, Issue 3, pp. 252-277, 2011. Elsevier.
– J. B. Almeida, M. J. Frade, J. S. Pinto, S. Melo de Sousa. Rigorous Software Development - An Introduction to Program Verification. Springer, 2011. ISBN 978-0-85729-017-5.
– M. J. Frade, A. Saabas, T. Uustalu. Bidirectional data-flow analyses, type-systematically. In Proc. of 2009 ACM SIGPLAN Wksh. on Partial Evaluation and Semantics-Based Program Manipulation, PEPM 2009 (Savannah, GA, Jan. 2009), pp. 141-149. ACM Press, 2009.
– M. J. Frade, A. Saabas, T. Uustalu. Foundational certification of data-flow analyses. In First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE'07 (Shanghai, June 2007) , pp. 107-116. IEEE CS Press, 2007. © IEEE
– J. Espírito Santo, M. J. Frade, L. Pinto. Structural Proof Theory as Rewriting. In Term Rewriting and Applications , volume 4098 of Lecture Notes in Computer Science. 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings. © Springer-Verlag
– G. Barthe, M. J. Frade, E. Giménez, L. Pinto, T. Uustalu. Type-based termination of recursive definitions. In Mathematical Structures in Computer Science , v. 14, n. 1, pp. 97-141, 2004. © Cambridge Univ. Press
– M. J. Frade. Type-Based Termination of Recursive Definitions and Constructor Subtyping in Typed Lambda Calculi. PhD Thesis. Universidade do Minho, Departamento de Informática, 2003.
– G. Barthe, M.J. Frade. Constructor Subtyping. In Programming Languages and Systems , volume 1574 of Lecture Notes in Computer Science. 8th European Symposium On Programming ESOP´99, held as a part of ETAPS'99, Amesterdam. © Springer-Verlag
– M. J. Frade. Comportamento e Estado. MSc Thesis. Universidade do Minho, Departamento de Informática, 1994.
Technical Reports
– J. M. Veiga, M. J. Frade. TreeCycle: a Sonar plugin for design quality assessment of Java programs. Technical Report CROSS-10.07-1. Universidade do Minho, 2010.
– M. J. Frade, J. S. Pinto. Verification Conditions for Source-level Imperative Programs. Technical Report DI-CCTC-08-02, 2008.
– G. Barthe, M.J. Frade. Constructor Subtyping (extended version). Departamento de Informática, Universidade of Minho, 1999.