Simão Melo de Sousa

I moved to the University of Algarve - please consult my new institutional webpage for updated information

---

Position

Short Resumé

• Agregação (Portuguese Habilitation / HDR) in Computer Science from the University of Beira Interior, Portugal.
• PhD in Computer Science from the Nice-Sophia Antipolis University (France), as a student of the Lemme Project of the INRIA Sophia Antipolis, France. "Reconhecimento" by the University of Beira Interior.
• Diplôme d'Etudes Approfondies (French Research Oriented Master degree) en Informatique Fondamentale (langages, programmation et traduction), from the University of Orléans-France. Equivalence with the Mestrado em Ciência da Computação from the University of Minho.
• Maitrise d'Informatique Fondamentale (French Undergraduate degree) from the University of Orléans-France. Equivalence with the Licenciatura de Ciências dos Computadores from Faculdade de Ciências of the University of Porto.

Teaching

---

Currently Teaching

BsC Program

• Lógica Computacional (Computational Logic)
• Teoria da Computação (Computation Theory)
• Programação Funcional (Functional Programming)

Master Program

• Desenho de Linguagens de Programação e de Compiladores (Programming Languages and Compilers Design)
• Segurança e Fiabilidade de Software (Software Reliability and Security)

PhD Program

• Teoria da Prova e da Programação (Proof and Programming Theory)
• Programação Certificada (Certified Programming)

Past Teaching

Seminars / Advanced Courses

• Certified Programming in the heavy presence of pointers - The case for Union-Find
• Functions should travel first-class
• Software Reliability and Security - The Formal Verification perspective (Release/LISP)
• Deductive Verification with Why3
• Software Security in the Era of the Internet of Things
• Functional Programming with OCaml
• Introduction to Blockchains

PhD Program

• Teoria da Prova e da Programação (Proof and Programming Theory) (2019-2020), (2016-2017), (2015-2016), (2014-2015), (2013-2014), (2012-2013), (2011-2012).
• Programação Certificada (Certified Programming) (2019-2020), (2016-2017), (2015-2016), (2014-2015), (2012-2013), (2011-2012).
• (2019-2020)

Master Program

• Computação Fiável (Formal Methods - Program Semantics and Verification) (2015-2016) (2013-2014) (2012-2013) (2011-2012) (2009-2010) (2008-2009) (2007-2008)
• Desenho de Linguagens de Programação e Compiladores (Programming Language Design and Compilation) (2015-2016))
• Computação Segura (Applied Cryptography) (2012-2013) (2008-2009) (2007-2008)
• Computação Ubíqua (Ubiquitous Programming) (2008-2009)
• Computação Fiável e Segura (Secure and Reliable Computing) (2005-2006)
• Fundamentos da Computação (Foundation of Computing) (2003-2004)

BSc Program

• Processamento de Linguagens (Formal Language Processing) (2019-2020),(2018-2019), (2016-2017), (2015-2016), (2014-2015).
• Lógica Computacional (Computational Logic) (2019-2020), (2018-2019), (2016-2017), (2015-2016), (2014-1015).
• Teoria da Computação (Computation Theory) (2015-2016), (2014-2015), (2013-2014), (2012-2013), (2011-2012), (2008-2009). (2007-2008)
• Engenharia de Software (Software Engineering) (2010-2011)
• Linguagens Formais e Compilação (Compilers Design) (2012-2013) (2011-2012) (2008-2009) (2007-2008) (2006-2007)
• Compiladores (Compiler Design - in the 5 years long BSc Program) (2005-2006) (2004-2005) (2003-2004)
• Fiabilidade dos Sistemas Informáticos (Computer System Reliability - in the 5 years long BSc Program) (2005-2006)
• Teoria da Computação (Computation Theory - in the 5 years long BSc Program) (2006-2007) (2005-2006) (2003-2004)
• (∗) Programação (Introduction to Programming) (2009-2010)
• Tecnologias da Comunicação Humana (Human-Computer Communication Technologies - in the 5 years long BSc Program) (2004-2005)
• Programação III (Programming and Programming Tools - in the 5 years long BSc Program) (2003-2004)
• Programação para as Engenharias (em C) (Introduction to (C) Programming for Engineers) (2004-2005)
• (∗) Programação e Algoritmos (Introduction to algorithms - in the 5 years long BSc Program) (2002-2003)
• Programação III - Currículo Antigo (C Programming) (1998-1999)
• Lógica (Mathématical Logic For the 5 years long BSc in Computer Science and Applied Mathematics) ((1998-1999)
• Programação (PASCAL) para as Engenharias (PASCAL Programming for Engineers) (1998-1999)
• (∗) Programação (PASCAL) para as Engenharias (PASCAL Programming for Engineers) (1997-1998)

I have been on a sabbatical leave from March 2017 to February 2018 and from March 2010 to February 2011.

Several of these courses are hosted in our corporate e-learning platform , please consult this platform for updated information - consulte os e-conteudos para informação actualizada : Moodle @ UBI

(∗) Practical Labs only.

Research

---

Research Goals

Design of modern, reliable and secure computer systems:

• methodologies
• tools
• applications

Research Area and Interests

COMPUTER SYSTEMS RELIABILITY

Deductive Program Verification, Formal Methods, Formal Specification and Verification, Proof Carrying Code, Formal Software Development, Applications to Safety Critical Systems (avionics, aerospace industry, medical systems, railways and public transport industry)

COMPUTER SYSTEMS SECURITY

Software Security, Language based Security, Blockchain, (verifiable) smart contracts for Blockchain, Mobile Code Security, Smart Cards, Applied Cryptography, CyberSecurity, Integrating Biometry with Strong Cryptography, Security in Cloud and Ubiquitous Computing.

COMPUTER AIDED REASONING

Program Logic, Automatic Demonstration, Proof Assistants, Computational Logic, Application to Computer Science.

PROGRAMING LANGUAGES DESIGN AND SEMANTICS

Type Systems, Operational Semantics, Functional Programming, (Static) Program Analysis, Compiler Design and Construction, Program Transformations, Domain Specific Languages.

Ongoing Projects

Research Oriented Projects

• EuroProofNet, CA20111 - European Research Network on Formal Proofs, COST Network, 2021-2025, Member
• CRISP, Consensus pRotocols envIronments and SPecifications. TRA project, Funded by Nova-Lincs. 2020-2021. PI/PR
• LEAF, Learning Foundations of Computer Science using OCaml. Funded by the OCaml Foundation. 2020-2021. co-PI/PR
• PREFAB, PRivacy and pErFormAnce concerns in Blockchain. TRA project, Funded by Nova-Lincs. 2020-2021. participant
• DIADEM, Deductive Verification Framework for Higher-order Programs.TRA project, Funded by Nova-Lincs. 2020-2021. participant
• C4 - Competence Center in Cloud Computing. 2018-2020 (CCDRC-P2020). Head of Research Line 4 and WorkPackage 1.1 Coordinator
• FRESCO - Formal Verification and Static Analysis of Tezos compliant Smart Contracts - 2018-2021. Funded by the Tezos Foundation. PI/PR.
• FACTOR - A Functional Programming Approach to Teaching in Portuguese Foundational Computing Courses - 2018-2020. Funded by the Tezos Foundation. PI/PR.

Innovation & Technology Transfer Oriented Projects

• GreenStamp: Mobile Energy Efficiency Services. 2021-2024. Funded by P2020. (local PI/PR)
• HORUS: Plataforma inteligente para mapeamento e avaliação de competências. 2021-2023. Funded by P2020. (local PI/PR)
• COPES, DSL for rapid prototyping, reasonning and simulation of consensus protocols and algorithms. Funded by coEnzyme, 2020-2021, PI/PR
• REDe FAROTIC - Fintech, CyberSecurity and Big Data technologies for regional entrepreneurship. 2019-2021 . Funded by the POCTEP program of INTERREG/FEDER. (Local PI/PR).

Past Projects

Research Oriented

• Formally designed and verified blockchains for private and anonymous transactions - 2018-2019. Funded by a stealth startup (PI/Principal Researcher).
• Software Repositories for Green Computing, FLAD/NSF funded. Member. 2016-2018.
• TACLe - Timing Analysis on Code-Level - ICT COST Action IC1202. Member. 2012-2016.
• FAVAS - A FormAl Verification PlAtform for real-time Systems. FCT-PTDC/EIA-CCO/105034/2008 (2010-2012). Coordination of the Work Package on source code and contract based methods. Partners: UBI, MITI/UMa, CCTC/DIUM (local PI/PR);
• CANTE - Descriptional and computational complexity of formal language FCT-PTDC/EIA-CCO/101904/2008 (2010-2012). Member. Partners: LIACC/DCC/FCUP;
• AVIACC - Analysis and Verification of Critical Concurrent Programs PTDC/EIA-CCO/117590/2010 (2012-2014). Member. Partners: CCTC/DIUM, LIACC/DCC/FCUP
• RESCUE - REliable and Safe Code execUtion for Embedded systems. PTDC/EIA /65862/2006 - 2008-2011. Principal Researcher and Coordinator. Partners: LIACC/FCUP, CISTER/IPP, HasLab/DIUM;
• VERIFICARD - formal verification of security properties for Java Card programs. (European) IST-funded project. Member. partners: University of Nijmegen (The Netherlands), INRIA (France), Technical University of Munich (Germany), University of Hagen (Germany), Swedish Institute of Computer Science (Sweden), Gemplus (France) and Schlumberger (France). 2000-2003.
• S-JAVA - Combination of formal tools for verifying security properties of Java Programs. Action de Recherche Coopérative (ARC) Project. Member. Partners: INRIA teams: Coq, Lande, Meije and Oasis the Semantics and Abstract Interpretation team from ENS Paris and Trusted Logic S.A. 2000-2001.
• FORMAVIE - Modélisation FORmelle et certification Sécuritaire pour MAchine VIrtuelle Embarquée. Member. Partners: Bull, Schlumberger, INRIA-Sophia Antipolis. 1999-2001.

Innovation & Technology Transfer Oriented

• QUIVVER - Centro de Competência em Qualidade de Processos em Engenharia de Software, Validação e Verificação de Software. Principal Researcher and Coordinator. Funded by : programa Sistema de Apoio a infra-estruturas Científicas e Tecnológicas (RESAICT), Programa Operacional Regional Centro. 2014. (Principal Researcher).
• Cloud based Software Testing and Quality Laboratory of The UBI Cloud Computing Center. Principal Researcher and Coordinator. Under the auspices of the Education and Science Ministry and the Adjunct Ministry for the Regional Development - 2014-2016.
• UATS - Usability and Accessibility Tests as a Service. Principal Researcher and Coordinator. In collaboration with PT Inovação in the context of the "Plano de Inovação 2014-2015" from Portugal Telecom;
• PROVA - From Requirements to Tests (2012-2014). Partners: Educed Lda, Critical Software and DIUM;
• SOFT-SIM - Sim Card by software in online electronic transaction systems (M2M); In collaboration with PT Inovação, in the context of the Plano de Inovação 2013-2014;
• PRICE - Privacy, Reliability and Integrity in Cloud Environments. In collaboration with PT Inovação in the context of the Plano de Inovação 2012-2014;
• PROSINAL - Rigorous Design, validation and certification of railways signaling systems. In collaboration with EFACEC;
• EVOLVE - Evolutionary Validation, Verification and Certification (EUREKA-ITEA2). In collaboration with Critical Software;
• STORK - Secure Identity Across Borders Linked (ICT Policy Support Programme), under the CIP (Competitiveness and Innovation Programme), and co-funded by the European Community. In collaboration with Multicert.

Publications

---

Authored Books

• Sylvain Conchon, Jean-Christophe Filliâtre, Simão Melo de Sousa (tradutor). Aprender a programar com OCaml, algoritmos e estruturas de dados. Edição Universidade da Beira Interior. 2021. ISBN: 978-989-654-764-6.
• José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa. "Rigorous Software Development - A Practical Introduction to Program Specification and Verification". Undergraduate Topics in Computer Science, Springer Verlag. First Edition, 2011, XIII, 307 p. 52 illus. ISBN 978-0-85729-018-2 (ebook) ISBN 978-0-85729-017-5 (print book).

Edited Books

• 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, ISBN: 978-972-745- 096-1.
• Vitor Santos, Mário Freire, Jong Hyuk Park, Simão Melo de Sousa (Eds.). Proceedings of the "International Symposium on Information Security - IS 2007". "On the Move to Meaningful Internet Systems 2007" Springer Verlag, LNCS 4803 e LNCS 4804, ISBN 978-3-540-76846-3 e ISBN 978-3-540-76835-7.
• Vitor Santos, Pedro Rangel Henriques, Simão Melo de Sousa (Eds.). Proceedings of the conference Corta’07 "COmpilers, Related Technologies and Applications". Universidade da Beira Interior. ISBN 978- 972-8790-70-7.
• Vitor Santos, Mário Freire, Simão Melo de Sousa (Eds.). Proceeedings of the "First International Workshop on Information Security - IS’06". In the Proceedings of "On the Move to Meaningful Internet Systems 2006: OTM 2006 Workshops, OTM Confederated International Workshops and Posters", LNCS 4277 e 4278. ISBN 3-540-48269-5 e 3-540-48273-3. Springer Verlag, 2006.

Journal Guest Edition

• Simão Melo de Sousa (Guest Ed.): Journal of Computer Science and Information Systems, Special Issue on Compilers, Related Technologies and Applications. Volume 5, Number 2, December 2008 ISSN: 1820- 0214.
• Maxime Crochemore, Gaël Dias, Simão Melo de Sousa (Guest Eds.). "Fouille de données textuelles : complexité, algorithmique et passage à l’échelle". Journal "Traitement Automatique des Langues", 2005, Volume 46, n.2.

Journals

• Rui Pereira, Hugo Matalonga, Marco Couto, Fernando Castor, Bruno Cabral, Pedro Carvalho, Simão Melo de Sousa and João Paulo Fernandes. GreenHub: a large-scale collaborative dataset to battery consumption analysis of android devices Empirical Software Engineering volume 26, Article number: 38 (2021)
• P. Neto, J. Tojal, J. Veríssimo, S. Melo de Sousa. Towards a Formally Verified Space Mission Software Using SPARK” ADA User Journal, Volume 40, Number 4, December 2019.
• P. Soares, A. Ravara, S. Melo de Sousa. Revisiting Concurrent Separation Logic. Journal of Logical and Algebraic Methods in Programming, Elsevier. 40 pages. Feb. 2017.
• V. Rodrigues, B. Akesson, M. Florido, S. Melo de Sousa,, J. P. Pedroso, P. Vasconcelos. Certifying Execution Time in Multicores. Science of Computer Programming Journal, Elsevier. 46 pages. 2015.
• N. .Moreira, D. Pereira, S. Melo de Sousa. Deciding Kleene Algebra Terms Equivalence in Coq. Journal of Logic and Algebraic Methods in Programming, Elsevier. 28 pages. 2015.
• Nuno Gaspar and Simão Melo de Sousa. "WebVm - A web-based host platform for pedagogical virtual machines". Special issue of the journal Informática na Educação: teoria& prática Porto Alegre, v.12, n.1, jan./jun. 2009. ISSN digital 1982-1654, ISSN impresso 1516-084X.
• G. Barthe, P. Courtieu, G. Dufay, and S. Melo de Sousa. "Tool-Assisted Specification and Verification of Typed Low-Level Languages". Journal of Automated Reasoning - 35(4). 59 pages, p295-354 (2005).

Invited Talks/Keynotes

• Simão Melo de Sousa. Programming languages as tools. Invited talk, SLATE'22. Covilhã, Portugal. July 2022.
• 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 Logics; 2010, Porto - Portugal. January 2010.
• Simão Melo de Sousa. Tool Assisted Specification and Verification of a Subset of the .NET platform. Invited Talk . MSR Academic Summit, São Paulo - Brasil, May 2005.

International Conferences

• A. M. Dias, A. Ravara and S. Melo de Sousa. Supporting FLAT concepts in Learn-OCaml: seeing is believing, programming is understanding. OCaml worskhop of the Internacional Conference on Functional Programming, Ljubljana, Slovenia, 2022.
• P. Barroso, M. Pereira, A. Ravara, C. Silva, S. Melo de Sousa. A Logic Gallery in Why3. CiE 2021 - Computability in Eurpoe 2021. Contributed Talk. July 2021.
• N. Fonseca, J. P. Fernandes, M. Pires, S. Melo de Sousa. PACE: A DSL-based Approach to Manage Complex Build Pipelines. Proceedings of the 46th Euromicro Conference on Software Engineering and Advanced Applications (SEAA). August 2020. IEEE Xplore.
• R. Morais, P. Crocker, S. Melo de Sousa. A tool for implementing privacy in Nano. Proceedingds of the IEEE International Conference on Decentralized Applications and Infrastructures (DAPPS). August 2020. IEEE Xplore.
• L. Horta, J. Santos Reis, M. Pereira, S. Melo de Sousa. A Tool for Proving Michelson Smart Contracts in Why3. Proceedings of the 2020 IEEE International Conference on Blockchain (Blockchain-2020). November 2020.IEEE Xplore.
• J. Santos Reis, P. Crocker, S. Melo de Sousa. Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts. Proceedings of 2nd Workshop on Formal Methods for Blockchains. Host by the 32nd International Conference on Computer-Aided Verification. July 2020. OpenAccess Series in Informatics (OASIcs) by Dagstuhl.
• Hugo Matalonga, Bruno Cabral, Fernando Castor, Marco Couto, Rui Pereira, Simão Melo de Sousa, João Paulo Fernandes. GreenHub Farmer: Real-world data for Android Energy Mining. Proceedings of the 16th International Conference on Mining Software Repositories (MSR’19), Data Showcase Track.
• Paulo Vieira, Paul Crocker, Simão Melo de Sousa. Weak biometric authentication systems for smartphones and clouds reinforced by statistical measurements. In Actas do XXIV Congresso da Sociedade Portuguesa de Estatística, 2019.
• Paulo Vieira, Paul Crocker, Simão Melo de Sousa. e-Learning, Intelligence artificial and Blockchain. In European Conference on the Impact of Artificial Intelligence and Robotics. Published by Academic Conferences and Publishing International Limited Reading, UK.
• Jean-Christophe Filliâtre, Mário Pereira, Simão Melo de Sousa. Vérification de programmes OCaml fortement impératifs avec Why3. JFLA'2018, Jan 2018.
• J. Carvalho, S. Melo de Sousa, J-P. Fernandes, N. Pereira, L. F. Mendes, C. M. Figueiredo, C. R. Oliveira. Automated Analysis of Non-Functional Requirements for Web Applications, Proceedings of CSTI’2016. 2016.
• Pedro Soares, Simão Melo de Sousa and António Ravara. Revisiting Concurrent Separation Logic and Operational Semantics. In Proceedings of PDP'15 - 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing. IEEE Computer Society. Turku Finland. March 2015.
• Mário Pereira and Simão Melo de Sousa. Complexity checking of ARM programs, by deduction. In Proceedings of the 2014 ACM SIGAPP Symposium on Applied Computing, Software Verification and Testing (ACM SAC-SVT'14). March 2014, Gyeongju, Korea. ACM Press.
• J. Gouveia, P. Crocker, S. Melo de Sousa, and R. Azevedo. E-id authentication and uniform access to cloud storage service providers. In Proceedings of the 2013 IEEE 5th International Conference on Cloud Com- puting Technology and Science (CloudCom), CLOUDCOM ’13, 2013.
• Vítor Rodrigues, Benny Akesson, Mário Florido, Simão Melo de Sousa. Compositional Timing Analysis for Multicores Using Latency-Rate Abs- traction. Proceedings of Practical Aspects of Declarative Languages (PADL'2013). Lecture Notes in Computer Science - Springer Verlag. January 2013.
• David Pereira, Nelma Moreira, Simão Melo de Sousa. Deciding Regular Expressions (In-)Equivalence in Coq. Proceedings of RAMiCS,’2012. LNCS volume 7560. Springer.
• David Pereira, Nelma Moreira, Simão Melo de Sousa. A Decision Procedure for Regular Expressions (In)Equivalence in Coq. Automation in Proof Assistants 2012, TYPES-affiliated satellite workshop of ETAPS 2012. Sat 31 March - Sun 1 April, Tallinn, Estonia.
• André de Matos Pedro, Paul Crocker, Simão Melo de Sousa. Learning stochastic timed automata from sample executions. Proceedings of ISOLA’2012 - Greece - Crete - Heraklion- LNCS, Springer.
• André de Matos Pedro, Paul Crocker, Simão Melo de Sousa. T3S Tool - Learning stochastic discrete event systems from sample executions. Tool Demo Session - Proceedings of CIAA’2012. Porto, Portugal.
• Vítor Rodrigues, Mário Florido, Simão Melo de Sousa. Compositional Timing Analysis on Multi-Core Architectures. 18th edition of the SYNCHRON Workshop. November, 2011, Dammarie-les-Lys, France.
• 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.
• Vítor Rodrigues, João Pedro Pedroso, Mário Florido, Simão Melo de Sousa. Certifying Execution Time. (revised and extended version). Post-event Proceedings for selected papers of FOPARA 2011. LNCS, Springer.
• Nuno Gaspar, Vítor Gonçalves Rodrigues, Simão Melo de Sousa. Certifying Execution Time. Foundational and Practical Aspects of Ressource Analysis. FOPARA’2011, May 2011, Madrid Spain.
• 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 Leve- raging Applications of Formal Methods, Verification and Validation (ISOLA’2010) 18-20 October 2010 - Amirandes, Heraclion, Crete. Lecture Notes in Computer Science, 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), Lecture Notes on Computer Science, Winnipeg Manitoba, August 2010. Springer-Verlag.
• 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, Va- lencia, Spain.
• Paul Crocker, Vasco Nicolau, Simão Melo de Sousa. Sniffing with the Portuguese Identity Card, for fun and profit. Proceedings of ECIW’2010, Thessaloniki, Greece, July 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.
• 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.
• M. Barbosa, T. Brouard, S. Cauchie, S. Melo de Sousa. Secure Biometric Authentication with Improved Accuracy. Australasian Conference on Information Security and Privacy, ACISP 2008: 21-36. Lecture No- tes in Computer Science 5107 Springer. 2008, ISBN 978-3-540-69971-2.
• J. Gomes, D. Martins, S. Melo de Sousa, J. Sousa Pinto. Lissom, a Source Level Proof Carrying Code Platform. LICS’2006 affiliated Workshop PCC proceedings. Seattle, 2006.
• S. Cauchie, T. Brouard, S. Melo de Sousa. "Deux Approches de l ’acquisition et du traitement d’un signal biométrique cutané". Capteur 2005. 19-20/10/2005. Bourges, France.
• FME Subgroup on Education (convenor: J.N. Oliveira). "A survey of formal methods courses in European higher education". Teaching Formal Methods’ 04. Number 3294 in Lecture Notes in Computer Science, pages 235-248. Springer-Verlag, 2004.
• G. Barthe, P. Courtieu, G. Dufay, and S. Melo de Sousa. "Tool-Assisted Specification and Verification of the JavaCard Platform". In H. Kirchner and C. Ringeissen, editors, Proceedings of AMAST’02, LNCS 2422, pp 41-59. Springer-Verlag.
• G. Barthe, G. Dufay, L. Jakubiec, S. Melo de Sousa. "A formal correspondence between offensive and defensive JavaCard virtual machines". In A. Cortesi, editor, Proceedings of VMCAI’02, LNCS 2294, pp 32-45. Springer-Verlag.
• G. Barthe, G. Dufay, M. Huisman, S. Melo de Sousa. "Jakarta: a toolset for reasoning about JavaCard". In I. Attali and T. Jensen, editors, Proceedings of e-SMART’01, LNCS 2140. pp 2-18. Springer- Verlag.
• G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, S. Melo de Sousa. A Formal Executable Semantics of the JavaCard Platform. In D. Sands, editor, Proceedings of ESOP’01, LNCS 2028, pp 302-319. Springer- Verlag.
• G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, S. Melo de Sousa, S-W. Yu. "Formalization of the JavaCard Virtual Machine in Coq". In S. Drossopoulou et al, editor, Proceedings of FTfJP’00, pp 50-56, Cannes.

National Conferences

• P. Vieira, P. Crocker, S. Melo de Sousa. Weak biometric authentication systems for smartphones and clouds reinforced by statistical measurements. In Actas do XXIV Congresso da Sociedade Portuguesa de Estat\'{\i}stica, 2019.
• J.-C. Filliâtre, M. Pereira, S. Melo de Sousa. Vérification de programmes OCaml fortement impératifs avec Why3. JFLA'2018, Jan 2018.
• Vitor Pereira, Simão Melo de Sousa, Paul Crocker, Ricardo Azevedo. Criptografia Homomórfica como um Serviço: da Implementação à  sua Aplicação. Proceedings of Infórum’2013. September 2013, Évora.
• Mário Pereira, Jean-Christophe Filliâtre and Simão Melo de Sousa. ARMY: A deductive verification platform for ARM programs using Why3. INFORUM’2012. Caparica - Portugal. September 2012. Best Student Paper.
• André de Matos Pedro, Maria João Frade, Ana Paula Martins and Simão Melo de Sousa. Aprendizagem de processos semi-Markovianos generalizados: dos sistemas de eventos discretos estocásticos aos testes e à verificação. INForum 2011. 8-9th September 2011, Coimbra, Portugal.
• Vítor Rodrigues, Mário Florido and Simão Melo de Sousa. Back An- notation in Action: from WCET Analysis to Source Code Verification. INForum 2011. 8-9th September 2011, Coimbra, Portugal.
• 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.).
• 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.).
• Paul Crocker, Vasco Nicolau, Simão Melo de Sousa. A nova dimensão da entidade electrónica em Portugal. Congresso Nacional de Segurança e Defesa. Lisbon, May 2010.
• Joel Silva Carvalho and Simão Melo de Sousa. Verificação de Modelos em Programas HTL, INFORUM 2009 proceedings, Lisbon. September 2009.
• T. Brouard, H. Cardot, S. Cauchie, S. Melo de Sousa. Secure Biometric authentication way: a hybrid match-on-card system. In Proceedings of SINO’06 - Segurança Informática nas Organizações.
• D. Martins, S. Melo de Sousa. "LISSOM: Plataforma do Paradigma Proof Carrying Code para Execução Segura de Código Móvel". In Proceedings of SINO’05, "Segurança Informática nas Organizações", 2005, UBI. ISBN 972-8790-42-2.

Thesis

• Simão Melo de Sousa. "Proof of Programs, its art and its practice". Agregação/HDR/Habilitation. 2015
• Simão Melo de Sousa. "Outils et techniques pour la vérification formelle de la plate-forme JavaCard". PhD thesis, INRIA/Universidade de Nice-Sophia Antipolis, Fevereiro 2003.
• Simão Melo de Sousa, "Des Systèmes d’Aide à la Preuve: COQ et ISABELLE". Master thesis, Universidade de Orléans, Agosto 1995.

Other Publications

• Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich, Mário Pereira, Simão Melo de Sousa. A Toolchain to Produce Correct-by-Construction OCaml Programs. Jan 2018. HAL 01783851.
• Jean-Christophe Filliâtre, Mário Pereira, Simão Melo de Sousa. Vérification de programmes OCaml fortement impératifs avec Why3. Jan. 2018, HAL 01649989.
• Pedro Soares, António Ravara, Simão Melo de Sousa. Revisiting concurrent separation logic. Dec. 2017. arXiv:1712.01631.
• Pedro Soares, António Ravara, Simão Melo de Sousa. An Operational Semantics for Concurrent Separation Logic, Technical Report DCC- 2014-11, LIACC-UP, CITI & DI-FCT-UNL, LIACC-DI-FE, June, 2014.
• André de Matos Pedro, Maria João Frade, Simão Melo de Sousa. Learning generalized semi-Markov processes: >From stochastic discrete event systems to testing and verification, Technical Report DCC-2012-01, DCC-LIACC, Universidade do Porto, April, 2012.
• Nelma Moreira, David Pereira, Simão Melo de Sousa. Mechanization of an Algorithm for Deciding KAT Terms Equivalence, Technical Report DCC-2012-04, DCC - FC, Universidade do Porto, May, 2012.
• Sabine Broda, Nelma Moreira, Nuno Silva, Simão Melo de Sousa A Tool for Automatic Model Extraction of Ada/SPARK Programs (Part II) , Technical Report DCC-2011-02, DCC - FC, Universidade do Porto, October, 2011.
• 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.
• N. Moreira, D. Pereira, and S. Melo de Sousa. On the Mechanization of Kleene Algebra in Coq. Technical Report Dcc-2009-03, DCC- FC&LIACC, Universidade do Porto, 2009.
• S. Melo de Sousa, M. Freire, R. Cardoso. "Security Issues in Mobile code Paradigms", In Encyclopedia of Information Science and Technology. 2nd Edition. Mehdi Khosrow-Pour (ed.) Idea Group, Inc. 2006.