Jorge Sousa Pinto
Webpage of
About Me
I am an associate professor with habilitation at the Computer Science Department, Universidade do Minho, and a senior researcher at the High Assurance Software laboratory, HASLab/INESCTEC. I did a PhD in theoretical computer science at LIX, École Polytechnique, under the supervision of Ian Mackie and Radhia Cosout, working on Interaction Nets and the Geometry of Interaction. My research in recent years has focused on deductive program verification.
Here are my most recent efforts:
- Verification of distributed systems in Why3 with Why3-do
- A verified VCGen based on Dynamic Logic
Teaching
2022
Métodos Formais em Engenharia de Software
Mestrado em Engenharia Informática (MSc in Software Engineering)
An introduction to Formal Methods covering logic, automated reasoning, structural and behavioral modeling with Alloy, and deductive verification with Why3
2022
Algoritmos e Complexidade
Licenciatura em Engenharia Informática (BSc in Software Engineering)
An undergraduate course on Algorithms, essentialy covering the core (and some advanced) topics of AL–CS2013 in the IEEE/ACM curricula
2022
Verificação Formal
Mestrado em Engenharia Informática (MSc in Software Engineering)
An elective course on formal verification, covering assisted proofs with Coq,
Books and Edited Volumes
A Tribute to José Manuel Valença
I had the pleasure to be one of the editors of a volume published as a tribute to my colleague José Manuel Valença.
José Nuno Oliveira, Jorge Sousa Pinto, Luís Soares Barbosa, Pedro Rangel Henriques: A tribute to José Manuel Valença. J. Log. Algebraic Methods Program. 128: 100792 (2022).
An Introduction to Program Verification
José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo De Sousa. Springer Undergraduate Topics in Computer Science, 2011
LerNet Summer School
Revised, Selected Papers of the International LerNet ALFA Summer School 2008
Research Projects
A project exploring applications of formal methods in the context of robotics systems. FCT-funded.
The goal of this project is to develop a new framework that extends existing runtime monitoring infrastructures with features to guarantee safety and avoid security leaks, allowing for monitors to be automatically generated and deployed. FCT-funded.