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.
- 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.).
- 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
- 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.
- 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.
- 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á.
2008
- 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.
- 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.
|
|
 Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
|
|