Subsistema
Docentes Universitário
Unidade ID externa
NOVA Laboratory for Computer Science and Informatics (NOVA LINCS)
Regime
Exclusividade
Vínculo
CT em Funções Públicas por tempo indeterminado
Simão Melo de Sousa is a member of the Software Systems Group at Nova-LINCS.
Research Topics:
Formal Verification, Programming languages, Computer assisted reasonning,
Software Security and Reliability.
Google Scholar:
https://scholar.google.com/citations?user=nuuKV9cAAAAJ&hl=pt-PT
Short Bio:
Simão Melo de Sousa is an expert in security and reliability of computer systems.
In particular. He publishes and is actively developing research on the fundamentals
and the design of techniques and tools for the security and formal verification
of software. He is a co-author of the book "Rigorous software development - An
introduction to program verification" published in 2011 by Springer-Verlag.
He received his PhD from INRIA Sofia Antipolis / University of Nice Sofia Antipolis
with a thesis on the theme "Tools and techniques for the formal verification
of the JavaCard platform" and obtained his Habilitation by the University of
Beira Interior in 2015. He is a Full Professor at the Electronics and
Computer Science Department of the University of Algarve where he teaches
courses in the area of programming (foundational concepts, algorithms and
data structures and programming languages), software engineering, compilation,
computing fundamentals, formal verification, security and cryptography.
He is also a member of the NOVA-Lincs Research and coordinates the research
activities of the RELEASE group (Reliable and Secure Computation Lab).
He has scientifically coordinated several research projects (FCT, etc.) in
the area of software reliability and critical systems, information security,
testing and software quality (as-a-service), blockchain and smart contracts.
He was also visiting researcher at INRIA Paris-Saclay in 2010 and 2017.
He actively collaborates with several leading industrial partners, nationally
and internationally, in its area of expertise, in particular in the area of
critical systems, security, e-health, railway systems, avionics and aerospace.
In this context, he has successfully participated in several technology transfer initiatives.
Selected Publications:
- Pereira, R., Matalonga, H., Couto, M. et al. GreenHub: a large-scale collaborative dataset to battery consumption analysis of android devices. Empir Software Eng 26, 38 (2021). https://doi.org/10.1007/s10664-020-09925-5
- João Santos Reis, Paul Crocker, and Simão Melo de Sousa. Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 4:1-4:12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/OASIcs.FMBC.2020.4
- 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. 2018.
- H. Matalonga et al., "GreenHub Farmer: Real-World Data for Android Energy Mining," 2019 IEEE/ACM 16th International Conference on Mining Software Repositories (MSR), Montreal, QC, Canada, 2019, pp. 171-175, doi: 10.1109/MSR.2019.00034.
- L. P. Arrojado da Horta, J. Santos Reis, S. M. de Sousa and M. Pereira, "A tool for proving Michelson Smart Contracts in WHY3," 2020 IEEE International Conference on Blockchain (Blockchain), Rhodes, Greece, 2020, pp. 409-414, doi: 10.1109/Blockchain50366.2020.00059.
- R. Morais, P. Crocker and S. Melo de Sousa, "A Tool for Implementing Privacy in Nano," 2020 IEEE International Conference on Decentralized Applications and Infrastructures (DAPPS), Oxford, UK, 2020, pp. 159-163, doi: 10.1109/DAPPS49028.2020.00021.
Projetos
Projetos
2022 - 2023. LOX - Extending Learn-OCaml., INRIA/OCaml Software Foundation. Investigador responsável. Universidade da Beira Interior; Nova-Lincs.
2021 - 2023. GreenStamp: Mobile Energy services., P2020. Co-Investigador Responsável (Co-IR). Universidade da Beira Interior; Universidade de Coimbra.
2021 - 2023. HORUS: Plataforma inteligente para mapeamento e avaliação de competências, PT2020. Co-Investigador Responsável (Co-IR). Capgemini Engineering; Universidade da Beira Interior; Instituto Politécnico do Porto Instituto Superior de Engenharia do Porto.
2020 - 2022. LEAF - Learning Foundations of Compuyer Science using OCaml. Investigador responsável. Universidade da Beira Interior; Nova-Lincs; Universidade NOVA de Lisboa.
2019 - 2022. REDe FAROTIC - Fintech, CyberSecurity and Big Data technologies for regional entrepreneurship, POCTEP program of INTERREG/FEDER. Co-Investigador Responsável (Co-IR).
2018 - 2022. C4 - Competence Center in Cloud Computing. Linha 4., P2020. Investigador responsável. Universidade da Beira Interior.
2018 - 2022. C4 - Competence Center in Cloud Computing. Work Package 1.1, P2020. Investigador responsável. Universidade da Beira Interior.
2018 - 2022. FRESCO - Formal Verification and Static Analysis of Tezos compliant Smart Contracts. Investigador responsável. Universidade da Beira Interior; Nova-Lincs.
2020 - 2021. COPES, DSL for rapid prototyping, reasonning and simulation of consensus protocols and algorithms. Co-Investigador Responsável (Co-IR). Universidade da Beira Interior; Universidade NOVA de Lisboa; Nova-Lincs.
2018 - 2020. FACTOR - A Functional Programming Approach to Teaching in Portuguese Foundational Computing Courses. Investigador responsável. Universidade da Beira Interior; Universidade NOVA de Lisboa; Nova-Lincs.
2014 - 2016. QUIVVER - Centro de Competência em Qualidade de Processos em Engenharia de Software, Validação e Verificação de Software, Sistema de Apoio a infra-estruturas Científicas e Tecnológicas (RESAICT) do Prog. Oper. Reg. Centro. Investigador responsável. Universidade da Beira Interior.
2010/02/01 - 2013/01/31. FAVAS: A FormAl Verification PlAtform for real-time Systems, 3599-PPCDT. Universidade da Madeira Madeira Interactive Technologies Institute; Universidade do Minho; Universidade da Beira Interior.
2012/05/01 - 2015/04/30. Análise e Verificação de Programas Concorrentes Críticos, 5876-PPCDTI. Universidade do Minho; Universidade do Minho Centro ALGORITMI; Instituto Politécnico do Porto Instituto Superior de Engenharia do Porto; Universidade do Porto Faculdade de Ciências.
2012 - 2014. PROVA - From Requirements to Tests, QREN. Investigador. Universidade da Beira Interior; Universidade do Minho; Universidade do Porto Laboratório de Inteligência Artificial e Ciência de Computadores; Universidade do Minho Laboratório de Software Confiável.
2010/05/01 - 2013/09/30. CANTE: Complexidade descriptiva e computacional de linguagens formais, 5876-PPCDTI. Universidade do Porto Faculdade de Ciências; Universidade do Porto Laboratório de Inteligência Artificial e Ciência de Computadores.
2010 - 2012. PROSINAL - Rigorous Design, validation and certification of railways signaling systems, QREN. Investigador. Universidade da Beira Interior; Efacec Power Solutions; Universidade do Porto.
2008/01/01 - 2011/06/30. TRAMANET: Gestão do Tráfego e da Confiança em Redes Peer-to-Peer, 5876-PPCDTI. Universidade da Beira Interior.
2008/01/01 - 2011/03/31. RESCUE, Execução Fiável e Segura de Programas em Sistemas Embebidos, 5876-PPCDTI. Universidade do Porto Faculdade de Ciências; Universidade do Porto Laboratório de Inteligência Artificial e Ciência de Computadores; Instituto Politécnico do Porto Instituto Superior de Engenharia do Porto; Universidade do Minho; Universidade da Beira Interior.
2005/05/01 - 2008/06/30. Sumarização Automática de Texto para Tecnologias Móveis, POSC. Universidade da Beira Interior; Universidade do Porto Laboratório de Inteligência Artificial e Ciência de Computadores.
2000/09/01 - 2003/02/28. OUTILS ET TECHNIQUES POUR LA VALIDATION DE PROPRIÉTÉS DE SÉCURITÉ.
Produções
Rui Morais (0000-0002-5040-4164); Crocker, Paul; Simão Melo de Sousa. 2023. "Echidna: A New Consensus Algorithm for Efficient State Machine Replication". Trabalho apresentado em THE FIFTH INTERNATIONAL CONFERENCE ON BLOCKCHAIN COMPUTING AND APPLICATIONS (BCCA 2023), apresentado por Rui Morais (0000-0002-5040-4164), Kuwait,24 de outubro, 2023.
Délcio Ferramenta; Paul Robert; Simão Melo de Sousa. Autor correspondente: Délcio Ferramenta. 2023. "Análise do Consumo de Energia de Aplicações Android". Em Atas da 14ª edição do INForum.
Rui Barata; Carlos Pinto; Simão Melo de Sousa. Autor correspondente: Rui Barata. 2023. "Programação com contractos no Learn-OCaml". Em Atas da 14ª edição do INFORUM, 2023.
Rui Pedro Bernardo Morais; Paul Andrew Crocker; Simão Melo De Sousa. 2023. "Echidna: A New Consensus Algorithm for Efficient State Machine Replication". https://doi.org/10.1109/BCCA58897.2023.10338927
Artur Miguel Dias; Ravara, António; Simão Melo de Sousa. Autor correspondente: Ravara, António. 2022. "Supporting FLAT Concepts in Learn-OCaml: Seeing is Believing; Programming is Understanding ". Trabalho apresentado em OCaml Worshop, ICFP'2022, Ljubljana, Slovenia,16 de setembro, 2022.
Pereira, Rui; Matalonga, Hugo; Couto, Marco; Castor, Fernando; Cabral, Bruno; Carvalho, Pedro; Melo de Sousa, Simão; Fernandes, João Paulo. 2021. "GreenHub: a large-scale collaborative dataset to battery consumption analysis of android devices". Empirical Software Engineering, 26 (3). https://doi.org/10.1007/s10664-020-09925-5
Morais, Rui; Crocker, Paul Andrew; Sousa, Simão Melo De. 2020. "A tool for implementing privacy in Nano".
Matalonga, Hugo; Cabral, Bruno; Castor, Fernando; Couto, Marco; Pereira, Rui; de Sousa, Simao Melo; Fernandes, Joao Paulo. 2019. "GreenHub Farmer: Real-World Data for Android Energy Mining". Em 2019 IEEE/ACM 16th International Conference on Mining Software Repositories (MSR).: IEEE. https://doi.org/10.1109/msr.2019.00034
P. Neto; J. Tojal; S. Veríssimo; Simão Melo de Sousa. Autor correspondente: P. Neto. 2019. "Towards a Formally Verified Space Mission Software Using SPARK". ADA User Journal,, 40 (4).
Soares, Pedro; Ravara, António; Melo de Sousa, Simão. 2017. "Revisiting concurrent separation logic". Journal of Logical and Algebraic Methods in Programming, 89: 41-66. https://doi.org/10.1016/j.jlamp.2017.02.004
Carvalho, Joel; de Sousa, Simao Melo; Fernandes, Joao Paulo; Pereira, Nuno; Mendes, Luis Filipe; Figueiredo, Carlos Manuel; Oliveira, Catia Raquel. 2016. "Automated analysis of non-functional requirements for web applications". Em 2016 11th Iberian Conference on Information Systems and Technologies (CISTI).: IEEE. https://doi.org/10.1109/cisti.2016.7521392
Rodrigues, Vítor; Akesson, Benny; Florido, Mário; de Sousa, Simão Melo; Pedroso, João Pedro; Vasconcelos, Pedro. 2015. "Certifying execution time in multicores". Science of Computer Programming, 111: 505-534. https://doi.org/10.1016/j.scico.2015.06.006
Moreira, Nelma; Pereira, David; Melo de Sousa, Simão. 2015. "Deciding Kleene algebra terms equivalence in Coq". Journal of Logical and Algebraic Methods in Programming, 84 (3): 377-401. https://doi.org/10.1016/j.jlamp.2014.12.004
Soares, Pedro; Ravara, Antonio; Sousa, Simao Melo de. 2015. "Revisiting Concurrent Separation Logic and Operational Semantics". Em 2015 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing.: IEEE. https://doi.org/10.1109/pdp.2015.85
Pereira, Mário; de Sousa, Simão Melo. 2014. "Complexity checking of ARM programs, by deduction". Em Proceedings of the 29th Annual ACM Symposium on Applied Computing - SAC '14.: ACM Press. https://doi.org/10.1145/2554850.2555012
Rodrigues, V.; Akesson, B.; Melo De Sousa, S.; Florido, M.. 2013. "A declarative compositional timing analysis for multicores using the latency-rate abstraction". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7752 LNCS: 43-59. https://doi.org/10.1007/978-3-642-45284-0_4
Gouveia, Joao; Crocker, Paul Andrew; Sousa, Simao Melo de; Azevedo, Ricardo. 2013. "E-Id Authentication and Uniform Access to Cloud Storage Service Providers". Em 2013 IEEE 5th International Conference on Cloud Computing Technology and Science.: IEEE. https://doi.org/10.1109/cloudcom.2013.71
Rodrigues, V.; Pedroso, J.P.; Florido, M.; De Sousa, S.M.. 2012. "Certifying execution time". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7177 LNCS: 108-125. https://doi.org/10.1007/978-3-642-32495-6_7
Moreira, N.; Pereira, D.; Melo De Sousa, S.. 2012. "Deciding regular expressions (in-)equivalence in Coq". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7560 LNCS: 98-113. https://doi.org/10.1007/978-3-642-33314-9_7
De Matos Pedro, A.; Crocker, P.A.; De Sousa, S.M.. 2012. "Learning stochastic timed automata from sample executions". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7609 LNCS (PART 1): 508-523. https://doi.org/10.1007/978-3-642-34026-0_38
Almeida, J.B.; Moreira, N.; Pereira, D.; De Sousa, S.M.; Almeida, José Bacelar; Moreira, Nelma; Pereira, David; Sousa, Simão Melo de. 2011. "Partial derivative automata formalized in coq". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6482 LNCS: 59-68. https://doi.org/10.1007/978-3-642-18098-9_7
Sousa, Simão. 2011. Rigorous Software Development.. http://link.springer.com/book/10.1007/978-0-85729-018-2
Carvalho, A.; Carvalho, J.; Pinto, J.S.; De Sousa, S.M.; Carvalho, André Ribeiro de; Carvalho, Joel; Pinto, Jorge Sousa; Sousa, Simão Melo de. 2010. "Model-checking temporal properties of real-time HTL programs". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6416 LNCS (PART 2): 191-205. https://doi.org/10.1007/978-3-642-16561-0_22
Crocker, P.; Nicolau, V.; De Sousa, S.M.. 2010. "Sniffing with the portuguese identify card for fun and profit". 9th European Conference on Information Warfare and Security 2010, ECIW 2010, 43-55. http://www.scopus.com/inward/record.url?eid=2-s2.0-84873122820&partnerID=MN8TOARS
Faculdade de Ciências. 2010. A tool for automatic model extraction of Ada/SPARK programs. This paper presents a brief description of the current work on a tool that analyses temporal behaviour of Ada/RavenSPARK programs. The approach takes as a basis two previous publications that introduce innovative methods in the field of verification of real-time systems. The development of a tool that automatically generates models (timed automata) from Ada/RavenSPARK source code and uses the mode. https://repositorio-aberto.up.pt/handle/10216/53339
Faculdade de Ciências. 2010. Partial Derivative Automata Formalized in Coq.. https://repositorio-aberto.up.pt/handle/10216/92883
André Carvalho; Nuno Silva; Simão Melo de Sousa; Nelma Moreira. 2010. A tool for automatic model extraction of Ada/SPARK programs. This paper presents a brief description of the current work on a tool that analyses temporal behaviour of Ada/RavenSPARK programs. The approach takes as a basis two previous publications that introduce innovative methods in the field of verification of real-time systems. The development of a tool that automatically generates models (timed automata) from Ada/RavenSPARK source code and uses the mode. https://hdl.handle.net/10216/53339
Nuno Gaspar; Simão Melo de Sousa; Rogério Reis. 2010. Timing analysis - from predictions to certificates. https://hdl.handle.net/10216/96297
Gaspar, Nuno; de Sousa, Simão Melo. 2009. "Uma plataforma de hospedagem baseada na Web para máquinas pedagógicas". https://doi.org/10.22456/1982-1654.12154
Barbosa, M.; Brouard, T.; Cauchie, S.; De Sousa, S.M.. 2008. "Secure biometric authentication with improved accuracy". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 5107 LNCS: 21-36. https://doi.org/10.1007/978-3-540-70500-0-3
de Sousa, S.M.. 2008. "The international journal published by ComSIS consortium". Computer Science and Information Systems, 5 (2). http://www.scopus.com/inward/record.url?eid=2-s2.0-70349696424&partnerID=MN8TOARS
Sousa, Simão. 2008. Proceedings of the conference Corta’08 "COmpilers, Related Technologies and Applications".
Barbosa, Manuel; Sousa, Simão Melo de; Brouard, Thierri; Cauchie, Stéphane. 2008. "Secure biometric authentication with improved accuracy". https://doi.org/10.1007/978-3-540-70500-0-3
Freire, M.M.; De Sousa, S.M.; Santos, V.; Park, J.H.; Freire, M.. 2007. "IS 2007 PC co-chairs' message". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 4804 LNCS (PART 2). http://www.scopus.com/inward/record.url?eid=2-s2.0-38349070264&partnerID=MN8TOARS
Sousa, Simão. 2007. "Proceedings of the conference Corta’07 "COmpilers, Related Technologies and Applications".
Gomes, João; Martins, Daniel; Sousa, Simão Melo de; Pinto, Jorge Sousa. 2006. "Lissom, a source level proof carrying code platform".
Barthe, Gilles; Courtieu, Pierre; Dufay, Guillaume; Melo de Sousa, Simão. 2006. "Tool-Assisted Specification and Verification of Typed Low-Level Languages". Journal of Automated Reasoning, 35 (4): 295-354. https://doi.org/10.1007/s10817-005-0084-6
Barthe, G.; Courtieu, P.; Dufay, G.; Melo De Sousa, S.. 2005. "Tool-assisted specification and verification of typed low-level languages". Journal of Automated Reasoning, 35 (4): 295-354. https://doi.org/10.1007/s10817-005-0084-6
Oliveira, J.N.. 2004. "A survey of formal methods courses in European higher education: The FME subgroup on education". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3294: 235-248. http://www.scopus.com/inward/record.url?eid=2-s2.0-35048903091&partnerID=MN8TOARS
Sousa, Simão. 2002. "Tool-Assisted Specification and Verification of the JavaCard Platform". https://doi.org/10.1007/3-540-45719-4_4
Sousa, Simão. 2002. "A formal correspondence between offensive and defensive JavaCard virtual machines". https://doi.org/10.1007/3-540-47813-2_3
