Using Internet technology for course support. - José Eduardo Pina Miranda; Jorge Sousa Pinto (ITiCSE, 1996)

Sequential and Concurrent Abstract Machines for Interaction Nets. - Jorge Sousa Pinto (FoSSaCS, 2000)

Combining interaction nets with externally defined programs. - Maribel Fernández; Ian Mackie; Jorge Sousa Pinto (APPIA-GULP-PRODE, 2001)

Parallel Evaluation of Interaction Nets with MPINE. - Jorge Sousa Pinto (RTA, 2001)

Parallel Implementation Models for the lambda-Calculus Using the Geometry of Interaction. - Jorge Sousa Pinto (TLCA, 2001)

A Higher-Order Calculus for Graph Transformation. - Maribel Fernández; Ian Mackie; Jorge Sousa Pinto (TERMGRAPH, 2002)

Encoding Linear Logic with Interaction Combinators. - Ian Mackie; Jorge Sousa Pinto (Inf. Comput., 2002)

Weak reduction and garbage collection in interaction nets. - Jorge Sousa Pinto (WRS, 2003)

A Framework for Point-Free Program Transformation. - Alcino Cunha; Jorge Sousa Pinto; José Proença (IFL, 2005)

Point-free Program Transformation. - Alcino Cunha; Jorge Sousa Pinto (Fundam. Informaticae, 2005)

Recursion patterns and time-analysis. - Manuel Barbosa; Alcino Cunha; Jorge Sousa Pinto (ACM SIGPLAN Notices, 2005)

A Local Graph-rewriting System for Deciding Equality in Sum-product Theories. - José Bacelar Almeida; Jorge Sousa Pinto; Miguel Vilaça (TERMGRAPH@ETAPS, 2006)

Visual Programming with Recursion Patterns in Interaction Nets. - Ian Mackie; Jorge Sousa Pinto; Miguel Vilaça (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2007)

Token-passing Nets for Functional Languages. - José Bacelar Almeida; Jorge Sousa Pinto; Miguel Vilaça (WRS@RDP, 2007)

A Tool for Programming with Interaction Nets. - José Bacelar Almeida; Jorge Sousa Pinto; Miguel Vilaça (RULE@RDP, 2007)

Visual Programming with Interaction Nets. - Abubakar Hassan; Ian Mackie; Jorge Sousa Pinto (Diagrams, 2008)

Deriving Sorting Algorithms - José Bacelar Almeida; Jorge Sousa Pinto (CoRR, 2008)

Lissom, a Source Level Proof Carrying Code Platform - João Gomes; Daniel Martins; Simão Melo de Sousa; Jorge Sousa Pinto (CoRR, 2008)

Preface. - Günter Kniesel; Jorge Sousa Pinto (RULE, 2008)

Verifying Cryptographic Software Correctness with Respect to Reference Implementations. - José Bacelar Almeida; Manuel Barbosa; Jorge Sousa Pinto; Bárbara Vieira (FMICS, 2009)

Iterators, Recursors and Interaction Nets - Ian Mackie; Jorge Sousa Pinto; Miguel Vilaça (CoRR, 2009)

Program Verification in SPARK and ACSL: A Comparative Case Study. - Eduardo Brito; Jorge Sousa Pinto (Ada-Europe, 2010)

Model-Checking Temporal Properties of Real-Time HTL Programs. - André Carvalho; Joel Carvalho; Jorge Sousa Pinto; Simão Melo de Sousa (ISoLA (2), 2010)

Contract-Based Slicing. - Daniela Carneiro da Cruz; Pedro Rangel Henriques; Jorge Sousa Pinto (ISoLA (1), 2010)

Contract-Based Slicing Helps on Safety Reuse. - Sergio Areias; Daniela Carneiro da Cruz; Jorge Sousa Pinto (ICPC, 2010)

GamaSlicer: an online laboratory for program verification and analysis. - Daniela Carneiro da Cruz; Pedro Rangel Henriques; Jorge Sousa Pinto (LDTA, 2010)

Safe Integration of Annotated Components in Open Source Projects. - Sergio Areias; Daniela Carneiro da Cruz; Pedro Rangel Henriques; Jorge Sousa Pinto (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010)

A Deductive Verification Platform for Cryptographic Software. - Manuel Barbosa; Jorge Sousa Pinto; Jean-Christophe Filliâtre; Bárbara Vieira (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010)

Deductive verification of cryptographic software. - José Bacelar Almeida; Manuel Barbosa; Jorge Sousa Pinto; Bárbara Vieira (Innov. Syst. Softw. Eng., 2010)

GammaPolarSlicer. - Sergio Areias; Daniela Carneiro da Cruz; Pedro Rangel Henriques; Jorge Sousa Pinto (Comput. Sci. Inf. Syst., 2011)

Verification conditions for source-level imperative programs. - Maria João Frade; Jorge Sousa Pinto (Comput. Sci. Rev., 2011)

Rigorous Software Development - An Introduction to Program Verification. - José Bacelar Almeida; Maria João Frade; Jorge Sousa Pinto; Simão Melo de Sousa (Springer, 2011)

An Approach to Model Checking Ada Programs. - José Miguel Faria; João Martins; Jorge Sousa Pinto (Ada-Europe, 2012)

Verification conditions for single-assignment programs. - Daniela Carneiro da Cruz; Maria João Frade; Jorge Sousa Pinto (SAC, 2012)

Using Term Rewriting to Solve Bit-Vector Arithmetic Problems - (Poster Presentation). - Iago Abal; Alcino Cunha; Joe Hurd; Jorge Sousa Pinto (SAT, 2012)

Assertion-based slicing and slice graphs. - José Bernardo Barros; Daniela Carneiro da Cruz; Pedro Rangel Henriques; Jorge Sousa Pinto (Formal Aspects Comput., 2012)

Towards a mostly-automated prover for bit-vector arithmetic. - Iago Abal; Jorge Sousa Pinto (C3S2E, 2013)

Interactive Verification of Safety-Critical Software. - Daniela Carneiro da Cruz; Pedro Rangel Henriques; Jorge Sousa Pinto (COMPSAC, 2013)

Formal verification of side-channel countermeasures using self-composition. - José Bacelar Almeida; Manuel Barbosa; Jorge Sousa Pinto; Bárbara Vieira (Sci. Comput. Program., 2013)

Towards a Runtime Verification Framework for the Ada Programming Language. - André de Matos Pedro; David Pereira; Luís Miguel Pinho; Jorge Sousa Pinto (Ada-Europe, 2014)

A Bounded Model Checker for SPARK Programs. - Cláudio Belo Lourenço; Maria João Frade; Jorge Sousa Pinto (ATVA, 2014)

Formal Verification of kLIBC with the WP Frama-C Plug-in. - Nuno Carvalho; Cristiano da Silva Sousa; Jorge Sousa Pinto; Aaron Tomb (NASA Formal Methods, 2014)

A Compositional Monitoring Framework for Hard Real-Time Systems. - André de Matos Pedro; David Pereira; Luís Miguel Pinho; Jorge Sousa Pinto (NASA Formal Methods, 2014)

CAOVerif: An open-source deductive verification platform for cryptographic software implementations. - José Bacelar Almeida; Manuel Barbosa; Jean-Christophe Filliâtre; Jorge Sousa Pinto; Bárbara Vieira (Sci. Comput. Program., 2014)

Monitoring for a Decidable Fragment of MTL-∫. - André de Matos Pedro; David Pereira; Luís Miguel Pinho; Jorge Sousa Pinto (RV, 2015)

Studying Verification Conditions for Imperative Programs. - Cláudio Belo Lourenço; Si-Mohamed Lamraoui; Shin Nakajima 001; Jorge Sousa Pinto (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2015)

Logic-based schedulability analysis for compositional hard real-time embedded systems. - André de Matos Pedro; David Pereira; Luís Miguel Pinho; Jorge Sousa Pinto (SIGBED Rev., 2015)

Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach. - Cláudio Belo Lourenço; Maria João Frade; Jorge Sousa Pinto (ESOP, 2016)

A Single-Assignment Translation for Annotated Programs. - Cláudio Belo Lourenço; Maria João Frade; Jorge Sousa Pinto (CoRR, 2016)

Formal Verification With Frama-C: A Case Study in the Space Software Domain. - Rovedy Aparecida Busquim e Silva; Nanci Naomi Arai; Luciana Akemi Burgareli; José Maria Parente de Oliveira; Jorge Sousa Pinto (IEEE Trans. Reliab., 2016)

SMT-based schedulability analysis using RMTL-∫. - André de Matos Pedro; David Pereira; Luís Miguel Pinho; Jorge Sousa Pinto (SIGBED Rev., 2017)

A Generalized Approach to Verification Condition Generation. - Cláudio Belo Lourenço; Maria João Frade; Shin Nakajima 001; Jorge Sousa Pinto (COMPSAC (1), 2018)

K-Taint: An Executable Rewriting Logic Semantics for Taint Analysis in the K Framework. - Md. Imran Alam; Raju Halder; Harshita Goswami; Jorge Sousa Pinto (ENASE, 2018)

Runtime verification of autopilot systems using a fragment of MTL- $${ int }$$ ∫. - André de Matos Pedro; Jorge Sousa Pinto; David Pereira; Luís Miguel Pinho (Int. J. Softw. Tools Technol. Transf., 2018)

A generalized program verification workflow based on loop elimination and SA form. - Cláudio Belo Lourenço; Maria João Frade; Jorge Sousa Pinto (FormaliSE@ICSE, 2019)

Testing for Race Conditions in Distributed Systems via SMT Solving. - João Carlos Pereira; Nuno Machado; Jorge Sousa Pinto (TAP@STAF, 2020)

Real-time MTL with durations as SMT with applications to schedulability analysis. - André de Matos Pedro; Martin Leucker; David Pereira; Jorge Sousa Pinto (TASE, 2020)

A deductive reasoning approach for database applications using verification conditions. - Md. Imran Alam; Raju Halder; Jorge Sousa Pinto (J. Syst. Softw., 2021)

Why3-do: The Way of Harmonious Distributed System Proofs. - Cláudio Belo Lourenço; Jorge Sousa Pinto (ESOP, 2022)

A tribute to José Manuel Valença. - José Nuno Oliveira; Jorge Sousa Pinto; Luís Soares Barbosa; Pedro Rangel Henriques (J. Log. Algebraic Methods Program., 2022)

A verified VCGen based on dynamic logic: An exercise in meta-verification with Why3. - Maria João Frade; Jorge Sousa Pinto (J. Log. Algebraic Methods Program., 2023)

Auto-active verification of distributed systems and specification refinements with Why3-do. - Cláudio Belo Lourenço; Jorge Sousa Pinto (Sci. Comput. Program., 2026)