Books

  • José Carlos Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa. Rigorous Software Development, An Introduction to Program Verification. Series: Undergraduate Topics in Computer Science, Springer. 1st Edition., 2011, XIII, 307 p. 52 illus. ISBN: 978-0-85729-017-5.

  • Simão Melo de Sousa. Outils et Techniques pour la verification formelle da la plateforme Javacard. Édition Universitaires Européenes. February 2011. ISBN: 978-613-1-53931-2.

Papers in Journals

2011

  • J. Espírito Santo, A note on preservation of strong normalisation in the lambda-calculus. Theoretical Computer Science 412(11): 1027-1032, 2011.

  • J. Espírito Santo, L. Pinto. A calculus of multiary sequent terms. To appear in ACM Transactions on Computational Logic. 2011.

  • Jose Bernardo Barros, Daniela da Cruz, Pedro Rangel Henriques, and Jorge Sousa Pinto. Assertion-based Slicing and Slice Graphs. To appear in Formal Aspects of Computing, 2011.

2010

  • J. Almeida, M. Barbosa, J. Pinto, and B. Vieira. Deductive Verification of Cryptographic Software. Innovations in Systems and Software Engineering - a NASA Journal - 6(3): 203-218 Springer, 2010.

  • Sandra Alves, Maribel Fernandez, Mário Florido and Ian Mackie. Goedel's System T Revisited. Theoretical Computer Science, Elsevier Science, 2010.

2009

2008

  • Maria João Varanda, Pedro Rangel Henriques, Simão Melo de Sousa (Eds.). Proceedings of the conference Corta'08 "COmpilers, Related Technologies and Applications". IPB Publisher, 2008. ISBN:978-972-745-096-1. Edição de actas de conferência nacional.

  • David Pereira and Nelma Moreira. KAT and PHL in Coq (extended version). ComSIS journal (Computer Science and Information Systems), Volume 05, Issue 02 (December 2008). ISSN: 1820-0214.

Papers in Workshops and Conferences

2011

  • Nuno Gaspar, Vítor Gonçalves Rodrigues,Simão Melo de Sousa. Cerifying Execution Time. Foundational and Practical Aspects of Ressource Analysis. FOPARA'2011, May 2011, Madrid Spain.

  • Vítor Gonçalves Rodrigues, Mário Florido, Simão Melo de Sousa. A Functional Approach to Worst-Case Execution Time Analysis. Functional and (Constraint) Logic Programming - WFLP'2011. July 2011, Odense , Denmark.

2010

  • Eduardo Brito and Jorge Sousa Pinto. Program Verification in SPARK and ACSL: A Comparative Case Study - 15th International Conference on Reliable Software Technologies - Ada-Europe 2010.

  • Daniela da Cruz, Pedro Rangel Henriques and Jorge Sousa Pinto GamaSlicer? : an Online Laboratory for Program Verification and Analysis. Proceedings of the of the Tenth Workshop on Language Descriptions, Tools and Applications, LDTA 2010, Paphos, Cyprus, March 28-29, 2010.

  • Daniela da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto. Contract-Based Slicing. Proceedings of the 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'2010), p106-120. 18-20 October 2010 - Amirandes, Heraclion, Crete. Lecture Notes in Computer Science (LNCS-6415), Springer Verlag.

  • José Bacelar Almeida, Nelma Moreira, David Pereira, and Simão Melo de Sousa. Partial derivative automata formalized in Coq. In Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA 2010), number 6482 in Lecture Notes on Computer Science, pages 59-68, Winnipeg, MA, Canada, August, 2010. 2011. Springer-Verlag.

  • Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis. On the average number of states of partial derivative automata. In Yuan Gao, Hanlin Lu, Shinnosuke Seki, and Sheng Yu, editors, Developments in Language Theory, 14th International Conference, DLT 2010, London, ON, Canada, August 17-20, 2010. Proceedings, volume 6224 of Lecture Notes on Computer Science, pages 112-123, London, ON, Canada, August 2010. Springer-Verlag. DOI:10.1007/978-3-642-14455-4 12.

  • Eva Maia, Nelma Moreira, and Rogério Reis. Inferência de tipos em Python. In Luís S. Barbosa and Miguel P. Correia, editors, Inforum, Simpósio de Informática, pages 515-518, Braga,Portugal, 9-10 Setembro 2010.

  • André Carvalho, Joel Carvalho, Jorge Sousa Pinto, Simão Melo de Sousa. Model-Checking Temporal Properties of Real-Time HTL Programs. Proceedings of the 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'2010) 18-20 October 2010 - Amirandes, Heraclion, Crete. Lecture Notes in Computer Science (LNCS-6415), Springer Verlag.

  • Nuno Gaspar, Rogério Reis and Simão Melo de Sousa. Timing Analysis - From Predictions to Certificates (nominated for the best student paper award). Actas do II Simpósio de Informática. INForum'2010. Universidade do Minho, Braga, 9-10 Setembro, 2010. Luís S. Barbosa, Miguel P. Correia (Eds.). P

  • Joaquim Tojal, Carlos Carloto, José Faria and Simão Melo de Sousa. Towards a Formally Verified Kernel Module. Actas do II Simpósio de Informática. INForum'2010. Universidade do Minho, Braga, 9-10 Setembro, 2010. Luís S. Barbosa, Miguel P. Correia (Eds.).

  • Simão Melo de Sousa. Design by Contracts approach to the formal verification of programs. Invited talk. Tech'Days 2010, Lisbon - Portugal. April 2010.

  • Simão Melo de Sousa. An introduction to program logic and the formal development of software. Invited talk. Days in Logic' 2010, Porto - Portugal. January 2010.

2009

  • J. B. Almeida, M. Barbosa, J. S. Pinto, and B. Vieira. Verifying Cryptographic Software Correctness with Respect to Reference Implementations. In M. Alpuente, B. Cook, and C. Joubert, editors, Proceedings of the 4th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'2009), volume 5825 of Lecture Notes in Computer Science, pages 37-52. Springer, 2009. Distinguished with the Best Paper award, from EASST.

  • Marco Almeida, Nelma Moreira, and Rogèrio Reis. Testing equivalence of regular languages. In Workshop on Descriptional Complexity of Formal Systems (DCFS09), Magdeburg, Germany, July 2009. Also in Electronic Proceedings in Theoretical Computer Science (eptcs 3) http://www.eptcs.org. DOI: 10.4204/EPTCS.3.4.

2008

  • J. Esprito Santo, S. Ghilezan, J. Ivetic. Characterizing strongly normalizing intuitionistic sequent terms. In M. Miculan, I. Scagnetto, F. Honsell (Eds.), Types for Proofs and Programs, International Conference TYPES 2007, Revised Selected Papers, Lecture Notes in Computer Science, volume 4941, pp. 85-99, Springer, 2008.

  • David Pereira and Nelma Moreira. Kat and PHL in COQ. In proceedings of Compilers, Related Technologies and and Applications (CoRTA2008)

  • David Pereira and Nelma Moreira. Ebdi in Coq. Days in Logic, 2008. Lisboa, Portugal, 2008.

  • David Pereira, Eugenio Oliveira, and Nelma Moreira. Formal modelling of emotions in Ebdi agents. In Eightth Workshop on Computational Logic in Multi-Agent Systems (CLIMA-VIII), LNAI, Porto, Portugal, 2008. Springer-Verlag.

  • Sandra Alves, Mário Florido, Ian Mackie and François-Régis Sinot. Minimality in a Linear Calculus with Iteration. The 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS), Electr. Notes Theor. Comput. Sci. 204: 163-179, 2008.

Tehcnical Reports

2010

Report DCC-2010-05, DCC-FC, Universidade do Porto, 2010.

2009

2008

  • Nelma Moreira, David Pereira and Simão Melo de Sousa. Mobile code security based on Kleene algebras and temporal logics. Technical Report DCC-2008-04, DCC - FC & LIACC, Universidade do Porto, August 2008.