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.

• M. J. Frade, J. S. Pinto. Verification Conditions for Source-level Imperative Programs. In Computer Science Review, Volume 5, Issue 2, 2011. Elsevier. DOI:10.1016/ j.cosrev.2011.02.002.

• 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.

• Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis. On the average state complexity of partial derivative automata. International Journal of Foundations of Computer Science, 2011.

• Sandra Alves, Maribel Fernandez, Mario Florido and Ian Mackie. Linearity and Iterator Types for Godel's System T. To appear in International Journal on Higher-Order and Symbolic Computation, Springer. 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

• J. Esprito Santo. The Lambda-Calculus and the Unity of Structural Proof Theory. Special Issue on Computability in Europe 2007, Theory of Computing Systems, 45:963-994, 2009

• Nuno Gaspar and Simão Melo de Sousa. WebVm - A web-based host platform for pedagogical virtual machines, INFORMÁTICA NA EDUCAÇÃO: teoria e prática. Porto Alegre, vol.12, n.1, jan./jun. 2009. ISSN digital 1982-1654, ISSN imp. 1516-084X (journal version of the IFIP-WCCE paper).

2008

• Simão Melo de Sousa, Guest editorial of Journal of Computer Science and Information Systems, Special Issue on Compilers, Related Technologies and Applications. Volume 5, Number 2, December 2008 ISSN: 1820-0214..

• 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

• J. Espírito Santo, Towards a canonical classical natural deduction system, in A. Dawar, H. Veith (Eds.), 19th EACSL International Conference Computer Science Logic (CSL 2010), Lecture Notes in Computer Science, Springer, vol. 6247, 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.

• Maia, C., Nogueira, L., Pinho, L., Evaluating Android OS for Embedded Real-Time Systems, Published in Proceedings of the 6th International Workshop on Operating Systems Platforms for Embedded Real-Time Applications, Brussels, Belgium, July 2010. pp. 63-70.

• Maia, C., Nogueira, L., Pinho, L., Short Paper: Experiences on the Implementation of a Cooperative Embedded System Framework, Published in Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems, Prague, Czech Republic, August 2010. pp. 70-72.

• Gonçalves, J., Ferreira, L., A Framework for QoS-Aware Service-based Mobile Systems, Published at Inforum 2010. II Simpósio de Informática, Luís S. Barbosa, Miguel P. Correia (eds), Braga, 9-10 Setembro, 2010, pp. 711.

• Gonçalves, J., Ferreira, L., Pinho, L., Silva, G., Handling Mobility on a QoS-Aware Service-based Framework for Mobile Systems, 2010 IEEE/IFIP International Conference on Embedded and Ubiquitous Computing, Hong-Kong, China, Dec 2010, pp. 97 - 104.

• Barros, A., Pinho, L., Managing contention of software transactional memory in real-time systems, Work in Progress (WiP) session of the 31st IEEE Real-Time Systems Symposium (RTSS 2010), San Diego, CA, USA, November 30 - December 3, 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.).

• Diogo Fialho, Nuno Gaspar, Jorge Sousa Pinto, Rogério Reis, Simão Melo de Sousa. Towards a Worst-Case Execution Time Calculation Platform with Certificate Production. Proceedings of EDCC'2010, Valencia, Spain.

• 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.

• D. Fialho , N. Gaspar, J. S.Pinto, R. Reis and S. Melo de Sousa. Worst-Case Execution Time: From predictions to certificates. Proceedings of the Days in Logic'2010. Porto - Portugal. January 2010.

• N. Moreira, D. Pereira and S. Melo de Sousa. Deciding regular expressions equivalence in Coq. Proceedings of the Days in Logic'2010. Porto - Portugal. January 2010.

• V. Rodrigues, M. Florido and S. Melo de Sousa. Pragmatic Program Transformation and Verification: an Abstract Interpretation Perspective. Proceedings of the Days in Logic'2010. Porto - Portugal. January 2010.

2009

• M. J. Frade, A. Saabas, T. Uustalu, Bidirectional data- ow analyses, type-systematically, PEPM09, ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Savannah, Georgia, USA, January 19-20, 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.

• J. B. Almeida, M. Barbosa, J. S. Pinto, and B. Vieira. Deductive Verification of Cryptographic Software. In Proceedings of the First NASA Formal Methods Symposium (NFM 2009), NASA conference publication CP-2009-215407.

• 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.

• D. Pereira. Encoding Kleene algebra (with tests) in Coq. Presentations session of the 18th EACSL Annual Conference on Computer Science Logic, CSL' 09 , Coimbra, Portugal, Sept. 2009.

• Nogueira, L., Pinho, L., Coelho, J., Coordinated Runtime Adaptations in Cooperative Open Real-Time Systems, Published in the 7th IEEE/IFIP International Conference on Embedded and Ubiquitous Computing, Aug. 2009, Vancouver, Canadá.

• Joel Silva Carvalho and Simão Melo de Sousa. Verificação de Modelos em Programas HTL, INFORUM 2009 proceedings, Lisbon. September 2009.

• André Passos, José Miguel Faria, Simão Melo de Sousa. Assessing the Formal Development of a Secure Partitioning Kernel with the B Method. ESA Workshop on Avionics Data, Control and Software Systems (ADCSS 2009) - Tracks on Formal Methods in Software Engineering.

• Nuno Gaspar and Simão Melo de Sousa. WebVm - A web-based host platform for pedagogical virtual machines, Proceedings of the IFIP WCCE - Bento Gonçalves, Brazil, July 2009.

2008

• J. Esprito Santo. The Lambda-Calculus and the Unity of Structural Proof Theory. Computability in Europe, 2008 (an extended version appears as a journal paper).

• L. Pinto, T. Uustalu. Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents, in M. Giese, A. Waaler (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods, 18th International Conference TABLEAUX 2009, Lecture Notes in Computer Science, volume 5607, pp. 295-309, Springer, 2009.

• 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.

• Diogo Fialho and Jorge Sousa Pinto, A comparative study of verification condition generators. In proceedings of Compilers, Related Technologies and and Applications (CoRTA2008)

• Daniela da Cruz, Pedro Rangel Henriques, and Jorge Sousa Pinto, Properties preservation during transformation. In proceedings of Compilers, Related Technologies and and Applications (CoRTA2008)

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

• Nuno Gaspar. Learning, teaching, playing with compiler construction - A web based host platform for target virtual machines. Proceedings of CoRTA'2008, IPB press,ISBN 978-972-745-096-1.

• 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.

• Nogueira, L., Pinho, L., Handling QoS Dependencies in Distributed Cooperative Real-Time Systems, Published in Proceedings of the 6th IFIP Working Conference on Distributed and Parallel Embedded Systems, Milan, Italy, September 2008.

• Nogueira, L., Pinho, L., Dynamic QoS Adaptation of Inter-Dependent Task Sets in Cooperative Embedded Systems, Published in Proceedings of the 2nd ACM International Conference on Autonomic Computing and Communication Systems, Turin, Italy, September 2008.

• M. Barbosa, T. Brouard, S. Cauchie, S. Melo de Sousa. Secure Biometric Authentication with Improved Accuracy. ACISP 2008: 21-36. Lecture Notes in Computer Science 5107 Springer. 2008, ISBN 978-3-540-69971-2.

Tehcnical Reports

2010

• André Carvalho, Nuno Silva, Simão Melo de Sousa, and Nelma Moreira. A tool for automatic model extraction of ada/spark programs. Technical

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

2009

• Marco Almeida, Nelma Moreira, Rogèrio Reis. Testing Regular Languages Equivalence. Technical Report DCC-2009-01, DCC - FC & LIACC, Universidade do Porto, 06/2009.

• Nelma Moreira, David Pereira, Simão Melo de Sousa. On the mechanization of Kleene algebra in Coq. Technical Report DCC-2009-03, DCC - FC & LIACC, Universidade do Porto, 04/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.

• Maria João Frade and Jorge Sousa Pinto, Verification conditions for source-level imperative programs. Technical Report DI-CCTC-08-01, Computer Science and Technology Center, Universidade do Minho, 2008