???global.info.a_carregar???
Identification

Personal identification

Full name
JORGE MIGUEL DE MATOS SOUSA PINTO

Author identifiers

Ciência ID
9E1F-C108-DE43
ORCID iD
0000-0002-0892-3577
Education
Degree Classification
2015/12
Concluded
 Agregação em Informática (Título de Agregado)
Universidade do Minho, Portugal
1998 - 2001
Concluded
 Doctorat de L’ Ecole Polytechnique, esp. Sémantique, Preuves, et Langages (Doutoramento)
Fundação para a Ciência e a Tecnologia, Portugal
"Paral lel Implementation with Linear Logic (Applications of Interaction Nets and of the Geometry of Interaction)" (THESIS/DISSERTATION)
 Très Honorable
2000 - 2000
Concluded
 The EU TMR LINEAR International Summer School (Curso médio)
Universidade dos Açores, Portugal
2000 - 2000
Concluded
 International Summer School on Applied Semantics (Curso médio)
Universidade do Minho, Portugal
1999 - 1999
Concluded
 20th International Summer School on Foundations of Secure Computation (Curso médio)
Adv. Study Institute of the NATO Science for Peace and Security Programme, Germany
1998 - 1998
Concluded
 10th European Summer School in Logic, Language and Information (Curso médio)
Universität des Saarlandes, Germany
1992 - 1995
Concluded
 Mestrado em Informática / Ciências da Computação (Mestrado)
Universidade do Minho, Portugal
"Construção de contextos em sistemas hierárquicos de representação de conhecimento" (THESIS/DISSERTATION)
1987 - 1992
Concluded
 Engenharia Electrotécnica e de Computadores (Licenciatura)
Universidade do Porto, Portugal
Projects

Contract

Designation Funders
2025/02/17 - 2026/08/17 VeriFixer: Automated Repair for Verification-Aware Programming Languages
2023.15557.PEX
Researcher
Instituto de Engenharia de Sistemas e Computadores Tecnologia e Ciência, Portugal
 Fundação para a Ciência e a Tecnologia
Ongoing
2018/07 - 2021/06 REASSURE: Secure Runtime Verification for Reliable Real-Time Embedded Systems
PTDC/EEI-COM/28550/2017
NORTE-01-0145-FEDER-028550
Researcher
Instituto de Engenharia de Sistemas e Computadores Tecnologia e Ciência, Portugal

Universidade do Minho, Portugal

Instituto Politécnico do Porto Centro de Investigação em Sistemas Computacionais Embebidos e de Tempo-Real, Portugal
Fundação para a Ciência e a Tecnologia
Ongoing
2018/07 - 2021/06 SAFER - Safety Verification for Robotic Software
POCI-01-0145-FEDER-029583
PTDC/CCI-INF/29583/2017
Researcher
Instituto de Engenharia de Sistemas e Computadores Tecnologia e Ciência, Portugal

Universidade do Minho, Portugal
Fundação para a Ciência e a Tecnologia
Ongoing
2013/01 - 2015/06 Languages and Tools for Critical Real-time Systems
NORTE-07-0124-FEDER-000062
Researcher
Universidade do Minho, Portugal
Concluded
2012/05 - 2015/04 AVIACC: Analysis and Verification of Critical Concurrent Programs
PTDC/EIA-CCO/117590/2010
Principal investigator
Universidade do Minho, Portugal

Universidade do Porto Laboratório de Inteligência Artificial e Ciência de Computadores, Portugal

Instituto Politécnico do Porto Centro de Investigação em Sistemas Computacionais Embebidos e de Tempo-Real, Portugal
Fundação para a Ciência e a Tecnologia
2012/06 - 2014/05 PROVA: Plataforma para a especificação e validação de requisitos
PROVA
Researcher
Universidade do Minho, Portugal

Universidade da Beira Interior, Portugal

Critical Software, Portugal
Governo de Portugal
Concluded
2010/03 - 2013/06 CROSS: An Infrastructure for Certification and Re-engineering of Open Source Software
PTDC/EIA-CCO/108995/2008
Researcher
Universidade do Minho, Portugal
 Fundação para a Ciência e a Tecnologia
Concluded
2010/02 - 2013/01 FAVAS - A FormAl Verification PlAtform for real-time Systems
PTDC/EIA-CCO/105034/2008
Researcher
Universidade do Minho, Portugal

Universidade da Madeira, Portugal

Universidade da Beira Interior, Portugal
Fundação para a Ciência e a Tecnologia
Concluded
2008/01 - 2011/03 RESCUE: Execução Fiável e Segura de Programas em Sistemas Embebidos
PTDC/EIA/65862/2006
Researcher
Universidade do Minho, Portugal

Universidade do Porto, Portugal

Instituto Politécnico do Porto, Portugal

Universidade da Beira Interior, Portugal
Fundação para a Ciência e a Tecnologia
Concluded
2009/01 - 2010/12 MATISSE: Reinvigorating Mathematics for the Information Society
PTDC/EIA/73252/2006
Researcher
Universidade do Minho, Portugal
 Fundação para a Ciência e a Tecnologia
Concluded
2008/01 - 2010/12 CACE: Computer-aided Cryptographic Engineering
CACE
Researcher
Universidade do Minho, Portugal
 European Commission
Concluded
2005/03 - 2009/02 LerNET: Engenharia de Linguagens e Desenvolvimento Formal de Software
II-0472-FA
Principal investigator
Universidade do Minho, Portugal
 European Commission
Concluded
2007/01 - 2008/12 Programação Visual
ProgVis
Principal investigator
Universidade do Minho, Portugal

University of London, United Kingdom
British Council

Fundação das Universidades Portuguesas
Concluded
2003/10 - 2006/12 PURe: Program Understanding and Reengineering: Calculi and Applications
POSI/CHS/44304/2002
Researcher
Universidade do Minho, Portugal
 Fundação para a Ciência e a Tecnologia
Concluded
2003/01 - 2005/12 APPSEM II: Semântica Aplicada
IST-2001-38957
Researcher
Universidade do Minho, Portugal
 European Commission
Concluded
Outputs

Publications

Book
  1. De Matos Pedro, A.; Pereira, D.; Pinho, L.M.; Pinto, J.S.. Towards a runtime verification framework for the Ada programming language. 2014.
    10.1007/978-3-319-08311-7_6
  2. Lourencço, C.B.; Frade, M.J.; Pinto, J.S.. A bounded model checker for SPARK programs. 2014.
    10.1007/978-3-319-11936-6_3
  3. Carvalho, N.; Da Silva Sousa, C.; Pinto, J.S.; Tomb, A.. Formal verification of kLIBC with the WP Frama-C plug-in. 2014.
    10.1007/978-3-319-06200-6_29
  4. De Matos Pedro, A.; Pereira, D.; Pinho, L.M.; Pinto, J.S.. A compositional monitoring framework for hard real-time systems. 2014.
    10.1007/978-3-319-06200-6_2
  5. Faria, J.M.; Martins, J.; Pinto, J.S.. An approach to model checking Ada programs. 2012.
    10.1007/978-3-642-30598-6_8
  6. Abal, I.; Cunha, A.; Hurd, J.; Sousa Pinto, J.. Using term rewriting to solve bit-vector arithmetic problems (Poster presentation). 2012.
    10.1007/978-3-642-31612-8_51
  7. Almeida, JB; Frade, MJ; Pinto, JS; Sousa, SMd. Rigorous Software Development - An Introduction to Program Verification. 2011.
    10.1007/978-0-85729-018-2
  8. Da Cruz, D.; Henriques, P.R.; Sousa Pinto, J.. Contract-based slicing. 2010.
    10.1007/978-3-642-16558-0_11
  9. Carvalho, A.; Carvalho, J.; Pinto, J.S.; De Sousa, S.M.. Model-checking temporal properties of real-time HTL programs. 2010.
    10.1007/978-3-642-16561-0_22
  10. Brito, E.; Sousa Pinto, J.. Program verification in SPARK and ACSL: A comparative case study. 2010.
    10.1007/978-3-642-13550-7_7
  11. Almeida, J.B.; Barbosa, M.; Sousa Pinto, J.; Vieira, B.. Verifying cryptographic software correctness with respect to reference implementations. 2009.
    10.1007/978-3-642-04570-7_5
  12. Hassan, A.; MacKie, I.; Sousa Pinto, J.. Visual programming with interaction nets. 2008.
    10.1007/978-3-540-87730-1_17
  13. Cunha, A.; Pinto, J.S.; Proença, J.. A framework for point-free program transformation. 2006.
    10.1007/11964681_1
  14. Pinto, J.S.. Parallel implementation models for the ¿-calculus using the Geometry of Interaction. 2001.
    10.1007/3-540-45413-6_30
  15. Pinto, J.S.. Parallel evaluation of Interaction Nets with MPINE. 2001.
    10.1007/3-540-45127-7_26
  16. Pinto, J.S.. Sequential and concurrent abstract machines for interaction nets. 2000.
    10.1007/3-540-46432-8_18
Book chapter
  1. Rovedy Aparecida Busquim e Silva; Nanci Naomi Arai; Luciana Akemi Burgareli; Jose Maria Parente de Oliveira; Jorge Sousa Pinto. "Exploring Frama-C Resources by Verifying Space Software". 2024.
    10.1007/978-3-031-55608-1_14
  2. Cláudio Belo Lourenço; Jorge Sousa Pinto. "Why3-do: The Way of Harmonious Distributed System Proofs". 114-142. Springer International Publishing, 2022.
    10.1007/978-3-030-99336-8_5
  3. João Carlos Pereira; Nuno Machado; Jorge Sousa Pinto. "Testing for Race Conditions in Distributed Systems via SMT Solving". 122-140. Springer International Publishing, 2020.
    10.1007/978-3-030-50995-8_7
Conference paper
  1. de Matos, A; Leucker, M; Pereira, D; Pinto, JS. "Real-time MTL with durations as SMT with applications to schedulability analysis". 2020.
    10.1109/tase49443.2020.00016
  2. Belo Lourenco, C; Frade, MJ; Sousa Pinto, J. "A Generalized Program Verification Workflow Based on Loop Elimination and SA Form". 2019.
    10.1109/formalise.2019.00017
  3. Lourenço, CB; Frade, MJ; Nakajima, S; Pinto, JS. "A Generalized Approach to Verification Condition Generation". 2018.
    10.1109/compsac.2018.00032
  4. Alam, MI; Halder, R; Goswami, H; Pinto, JS. "K-Taint: An Executable Rewriting Logic Semantics for Taint Analysis in the K Framework". 2018.
    10.5220/0006786603590366
  5. Lourenco, CB; Frade, MJ; Pinto, JS. "Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach". 2016.
    10.1007/978-3-662-49498-1_3
  6. Pedro, AD; Pereira, D; Pinho, LM; Pinto, JS. "Monitoring for a Decidable Fragment of MTL-integral". 2015.
    10.1007/978-3-319-23820-3_11
  7. Da Cruz, D.; Henriques, P.R.; Pinto, J.S.. "Interactive verification of safety-critical software". 2013.
    10.1109/compsac.2013.86
  8. Abal, I.; Pinto, J.S.. "Towards a mostly-automated prover for bit-vector arithmetic". 2013.
    10.1145/2494444.2494445
  9. Da Cruz, D.; Frade, M.J.; Pinto, J.S.. "Verification conditions for single-assignment programs". 2012.
    10.1145/2245276.2231977
  10. Barros, J.B.; Da Cruz, D.; Henriques, P.R.; Pinto, J.S.. "Assertion-based slicing and slice graphs". 2010.
    10.1109/SEFM.2010.18
  11. Da Cruz, D.; Henriques, P.R.; Pinto, J.S.. "GamaSlicer: An online laboratory for program verification and analysis". 2010.
    10.1145/1868281.1868284
  12. Areias, S.; Da Cruz, D.; Pinto, J.S.. "Contract-based slicing helps on safety reuse". 2010.
    10.1109/icpc.2010.44
  13. Barbosa, M; Almeida, JB; Pinto, JS; Vieira, B. "Deductive Verification of Cryptographic Software". 2009.
  14. Fernández, M; Mackie, I; Pinto, JS. "Combining interaction nets with externally defined programs". 2001.
  15. Miranda, J.E.P.; Pinto, J.S.. "Using Internet technology for course support". 1996.
    10.1145/237466.237548
Edited book
  1. Kniesel, G; Pinto, JS. Ninth International Workshop on Rule-Based Programming, RULE 2008, Hagenberg, Austria, July 14-18, 2008. 2012.
  2. Bove, A; Barbosa, LS; Pardo, A; Pinto, JS. Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised Tutorial Lectures. 2009.
    10.1007/978-3-642-03153-3
Journal article
  1. Frade, MJ; Pinto, JS. "A verified VCGen based on dynamic logic: An exercise in meta-verification with Why3". JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING (2023):
    10.1016/j.jlamp.2023.100871
  2. Oliveira, JN; Pinto, JS; Barbosa, LS; Henriques, PR. "A tribute to Jose Manuel Valenca". JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING (2022):
    10.1016/j.jlamp.2022.100792
  3. Alam, MI; Halder, R; Pinto, JS. "A deductive reasoning approach for database applications using verification conditions". JOURNAL OF SYSTEMS AND SOFTWARE (2021):
    10.1016/j.jss.2020.110903
  4. Pedro, AD; Pinto, JS; Pereira, D; Pinho, LM. "Runtime verification of autopilot systems using a fragment of MTL-". INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER (2018):
    10.1007/s10009-017-0470-5
  5. Matos Pedro, Ad; Pereira, D; Pinho, LM; Pinto, JS. "SMT-based schedulability analysis using RMTL-¿". SIGBED Review (2017):
    10.1145/3166227.3166234
  6. Busquim e Silva, RABE; Arai, NN; Burgareli, LA; Parente de Oliveira, JMP; Pinto, JS. "Formal Verification With Frama-C: A Case Study in the Space Software Domain". IEEE TRANSACTIONS ON RELIABILITY (2016): https://www.authenticus.pt/P-00K-THC.
    10.1109/tr.2015.2508559
  7. Pedro, AdM; Pereira, D; Pinho, LM; Pinto, JS. "Logic-based schedulability analysis for compositional hard real-time embedded systems". SIGBED Review (2015): https://www.authenticus.pt/P-00G-6CK.
    10.1145/2752801.2752808
  8. Lourenço, CB; Lamraoui, SM; Nakajima, S; Pinto, JS. "Studying Verification Conditions for Imperative Programs". ECEASST (2015): https://www.authenticus.pt/P-00K-9TS.
    10.14279/tuj.eceasst.72.1011.1004
  9. Almeida, J.B.; Barbosa, M.; Filliâtre, J.-C.; Pinto, J.S.; Vieira, B.. "CAOVerif: An open-source deductive verification platform for cryptographic software implementations". Science of Computer Programming 91 PART B (2014): 216-233. http://www.scopus.com/inward/record.url?eid=2-s2.0-84901798566&partnerID=MN8TOARS.
    10.1016/j.scico.2012.09.019
  10. Bacelar Almeida, J.; Barbosa, M.; Pinto, J.S.; Vieira, B.. "Formal verification of side-channel countermeasures using self-composition". Science of Computer Programming 78 7 (2013): 796-812. http://www.scopus.com/inward/record.url?eid=2-s2.0-84877581548&partnerID=MN8TOARS.
    10.1016/j.scico.2011.10.008
  11. Barros, J.B.; Da Cruz, D.; Henriques, P.R.; Pinto, J.S.. "Assertion-based slicing and slice graphs". Formal Aspects of Computing 24 2 (2012): 217-248. http://www.scopus.com/inward/record.url?eid=2-s2.0-84861577982&partnerID=MN8TOARS.
    10.1007/s00165-011-0196-1
  12. Kniesel, G.; Pinto, J.S.. "Preface". Electronic Notes in Theoretical Computer Science 290 (2012): 1-2. http://www.scopus.com/inward/record.url?eid=2-s2.0-84871255244&partnerID=MN8TOARS.
    10.1016/j.entcs.2012.11.007
  13. Frade, M.J.; Pinto, J.S.. "Verification conditions for source-level imperative programs". Computer Science Review 5 3 (2011): 252-277. http://www.scopus.com/inward/record.url?eid=2-s2.0-79957947758&partnerID=MN8TOARS.
    10.1016/j.cosrev.2011.02.002
  14. Areias, S.; da Cruz, D.; Henriques, P.R.; Pinto, J.S.. "GammaPolarSlicer". Computer Science and Information Systems 8 2 (2011): 477-499. http://www.scopus.com/inward/record.url?eid=2-s2.0-80755136749&partnerID=MN8TOARS.
    10.2298/CSIS110107006A
  15. Areias, S; da Cruz, DC; Henriques, PR; Pinto, JS. "Safe Integration of Annotated Components in Open Source Projects". ECEASST (2010): https://www.authenticus.pt/P-00A-8WT.
    10.14279/tuj.eceasst.33.460.448
  16. Barbosa, M; Pinto, JS; Filliâtre, JC; Vieira, B. "A Deductive Verification Platform for Cryptographic Software". ECEASST (2010): https://www.authenticus.pt/P-00A-8VG.
  17. Almeida, J.B.; Barbosa, M.; Pinto, J.S.; Vieira, B.. "Deductive verification of cryptographic software". Innovations in Systems and Software Engineering 6 3 (2010): 203-218. http://www.scopus.com/inward/record.url?eid=2-s2.0-77956423308&partnerID=MN8TOARS.
    10.1007/s11334-010-0127-y
  18. Almeida, J.B.; Pinto, J.S.; Vilaça, M.. "A Tool for Programming with Interaction Nets". Electronic Notes in Theoretical Computer Science 219 C (2008): 83-96. http://www.scopus.com/inward/record.url?eid=2-s2.0-55749108664&partnerID=MN8TOARS.
    10.1016/j.entcs.2008.10.036
  19. Almeida, J.B.; Pinto, J.S.; Vilaça, M.. "Token-passing Nets for Functional Languages". Electronic Notes in Theoretical Computer Science 204 C (2008): 181-198. http://www.scopus.com/inward/record.url?eid=2-s2.0-41649083728&partnerID=MN8TOARS.
    10.1016/j.entcs.2008.03.061
  20. Mackie, I; Pinto, JS; Vilaça, M. "Visual Programming with Recursion Patterns in Interaction Nets". ECEASST (2007): https://www.authenticus.pt/P-00A-8WW.
    10.14279/tuj.eceasst.6.66.49
  21. Fernández, M.; Mackie, I.; Pinto, J.S.. "A Higher-Order Calculus for Graph Transformation". Electronic Notes in Theoretical Computer Science 72 1 SPEC. IS (2007): 45-58. http://www.scopus.com/inward/record.url?eid=2-s2.0-34548321486&partnerID=MN8TOARS.
    10.1016/j.entcs.2002.09.005
  22. Almeida, J.B.; Pinto, J.S.; Vilaça, M.. "A Local Graph-rewriting System for Deciding Equality in Sum-product Theories". Electronic Notes in Theoretical Computer Science 176 1 (2007): 139-163. http://www.scopus.com/inward/record.url?eid=2-s2.0-34248563510&partnerID=MN8TOARS.
    10.1016/j.entcs.2006.10.031
  23. Cunha, A.; Pinto, J.S.. "Point-free program transformation". Fundamenta Informaticae 66 4 (2005): 315-352. http://www.scopus.com/inward/record.url?eid=2-s2.0-24044523566&partnerID=MN8TOARS.
  24. Barbosa, M.; Cunha, A.; Pinto, J.S.. "Recursion patterns and time-analysis". ACM SIGPLAN Notices 40 5 (2005): 45-54. http://www.scopus.com/inward/record.url?eid=2-s2.0-33745239605&partnerID=MN8TOARS.
    10.1145/1071221.1071226
  25. Pinto, J.S.. "Weak reduction and garbage collection in interaction nets". Electronic Notes in Theoretical Computer Science 86 4 (2003): 625-640. http://www.scopus.com/inward/record.url?eid=2-s2.0-18744382201&partnerID=MN8TOARS.
    10.1016/S1571-0661(05)82614-3
  26. Mackie, I.; Pinto, J.S.. "Encoding linear logic with interaction combinators". Information and Computation 176 2 (2002): 153-186. http://www.scopus.com/inward/record.url?eid=2-s2.0-0036707241&partnerID=MN8TOARS.
    10.1006/inco.2002.3163

Other

Other output
  1. A Single-Assignment Translation for Annotated Programs. 2016. Lourenço, CB; Frade, MJ; Pinto, JS. https://www.authenticus.pt/P-00K-9TR.
  2. Iterators, Recursors and Interaction Nets. 2009. Mackie, Ian; Pinto, JorgeSousa; Vilaça, Miguel. https://www.authenticus.pt/P-00G-6CJ.
  3. Deriving Sorting Algorithms. 2008. Almeida, JoseBacelar; Pinto, JorgeSousa. https://www.authenticus.pt/P-00G-6CG.
  4. Lissom, a Source Level Proof Carrying Code Platform. 2008. Gomes, Joao; Martins, Daniel; Sousa, SimaoMelode; Pinto, JorgeSousa. https://www.authenticus.pt/P-00G-6CH.
Activities

Consulting

Activity description Institution / Organization
2024/12/01 - 2025/01/31 External expert, later selected for Consensus Rapporteur, for the Open Call 2024 of the COST initiative of the EU Framework Program.