Jorge Sousa Pinto

66 papers A 4B 7C 2Misc 5Journal 25Unranked 20
YearRankTypeTitle / Venue / Authors
2026 J jnl
Auto-active verification of distributed systems and specification refinements with Why3-do.
Sci. Comput. Program.
Cláudio Belo Lourenço, Jorge Sousa Pinto
2023 J jnl
A verified VCGen based on dynamic logic: An exercise in meta-verification with Why3.
J. Log. Algebraic Methods Program.
Maria João Frade, Jorge Sousa Pinto
2022 J jnl
A tribute to José Manuel Valença.
J. Log. Algebraic Methods Program.
José Nuno Oliveira, Jorge Sousa Pinto, Luís Soares Barbosa, Pedro Rangel Henriques
2022 A conf
Why3-do: The Way of Harmonious Distributed System Proofs.
ESOP
Cláudio Belo Lourenço, Jorge Sousa Pinto
2021 J jnl
A deductive reasoning approach for database applications using verification conditions.
J. Syst. Softw.
Md. Imran Alam, Raju Halder, Jorge Sousa Pinto
2020 Misc conf
Real-time MTL with durations as SMT with applications to schedulability analysis.
TASE
André de Matos Pedro, Martin Leucker, David Pereira, Jorge Sousa Pinto
2020 — conf
Testing for Race Conditions in Distributed Systems via SMT Solving.
TAP@STAF
João Carlos Pereira, Nuno Machado, Jorge Sousa Pinto
2019 — conf
A generalized program verification workflow based on loop elimination and SA form.
FormaliSE@ICSE
Cláudio Belo Lourenço, Maria João Frade, Jorge Sousa Pinto
2018 — conf
A Generalized Approach to Verification Condition Generation.
COMPSAC (1)
Cláudio Belo Lourenço, Maria João Frade, Shin Nakajima, Jorge Sousa Pinto
2018 B conf
K-Taint: An Executable Rewriting Logic Semantics for Taint Analysis in the K Framework.
ENASE
Md. Imran Alam, Raju Halder, Harshita Goswami, Jorge Sousa Pinto
2018 J jnl
Runtime verification of autopilot systems using a fragment of MTL- $${\int }$$ ∫.
Int. J. Softw. Tools Technol. Transf.
André de Matos Pedro, Jorge Sousa Pinto, David Pereira, Luís Miguel Pinho
2017 J jnl
SMT-based schedulability analysis using RMTL-∫.
SIGBED Rev.
André de Matos Pedro, David Pereira, Luís Miguel Pinho, Jorge Sousa Pinto
2016 J jnl
A Single-Assignment Translation for Annotated Programs.
CoRR
Cláudio Belo Lourenço, Maria João Frade, Jorge Sousa Pinto
2016 J jnl
Formal Verification With Frama-C: A Case Study in the Space Software Domain.
IEEE Trans. Reliab.
Rovedy Aparecida Busquim e Silva, Nanci Naomi Arai, Luciana Akemi Burgareli, José Maria Parente de Oliveira, Jorge Sousa Pinto
2016 A conf
Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach.
ESOP
Cláudio Belo Lourenço, Maria João Frade, Jorge Sousa Pinto
2015 J jnl
Logic-based schedulability analysis for compositional hard real-time embedded systems.
SIGBED Rev.
André de Matos Pedro, David Pereira, Luís Miguel Pinho, Jorge Sousa Pinto
2015 B conf
Monitoring for a Decidable Fragment of MTL-∫.
RV
André de Matos Pedro, David Pereira, Luís Miguel Pinho, Jorge Sousa Pinto
2015 J jnl
Studying Verification Conditions for Imperative Programs.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Cláudio Belo Lourenço, Si-Mohamed Lamraoui, Shin Nakajima, Jorge Sousa Pinto
2014 B conf
A Bounded Model Checker for SPARK Programs.
ATVA
Cláudio Belo Lourenço, Maria João Frade, Jorge Sousa Pinto
2014 — conf
A Compositional Monitoring Framework for Hard Real-Time Systems.
NASA Formal Methods
André de Matos Pedro, David Pereira, Luís Miguel Pinho, Jorge Sousa Pinto
2014 J jnl
CAOVerif: An open-source deductive verification platform for cryptographic software implementations.
Sci. Comput. Program.
José Bacelar Almeida, Manuel Barbosa, Jean-Christophe Filliâtre, Jorge Sousa Pinto, Bárbara Vieira
2014 — conf
Formal Verification of kLIBC with the WP Frama-C Plug-in.
NASA Formal Methods
Nuno Carvalho, Cristiano da Silva Sousa, Jorge Sousa Pinto, Aaron Tomb
2014 Misc conf
Towards a Runtime Verification Framework for the Ada Programming Language.
Ada-Europe
André de Matos Pedro, David Pereira, Luís Miguel Pinho, Jorge Sousa Pinto
2013 J jnl
Formal verification of side-channel countermeasures using self-composition.
Sci. Comput. Program.
José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira
2013 B conf
Interactive Verification of Safety-Critical Software.
COMPSAC
Daniela Carneiro da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto
2013 — conf
Towards a mostly-automated prover for bit-vector arithmetic.
C3S2E
Iago Abal, Jorge Sousa Pinto
2012 Misc conf
An Approach to Model Checking Ada Programs.
Ada-Europe
José Miguel Faria, João Martins, Jorge Sousa Pinto
2012 J jnl
Assertion-based slicing and slice graphs.
Formal Aspects Comput.
José Bernardo Barros, Daniela Carneiro da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto
2012 — ed.
Ninth International Workshop on Rule-Based Programming, RULE 2008, Hagenberg, Austria, July 14-18, 2008
RULE
Günter Kniesel, Jorge Sousa Pinto
2012 A conf
Using Term Rewriting to Solve Bit-Vector Arithmetic Problems - (Poster Presentation).
SAT
Iago Abal, Alcino Cunha, Joe Hurd, Jorge Sousa Pinto
2012 Misc conf
Verification conditions for single-assignment programs.
SAC
Daniela Carneiro da Cruz, Maria João Frade, Jorge Sousa Pinto
2011 J jnl
GammaPolarSlicer.
Comput. Sci. Inf. Syst.
Sergio Areias, Daniela Carneiro da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto
2011 — book
Rigorous Software Development - An Introduction to Program Verification.
José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa
2011 J jnl
Verification conditions for source-level imperative programs.
Comput. Sci. Rev.
Maria João Frade, Jorge Sousa Pinto
2010 J jnl
A Deductive Verification Platform for Cryptographic Software.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Manuel Barbosa, Jorge Sousa Pinto, Jean-Christophe Filliâtre, Bárbara Vieira
2010 B conf
Assertion-based Slicing and Slice Graphs.
SEFM
José Bernardo Barros, Daniela Carneiro da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto
2010 A conf
Contract-Based Slicing Helps on Safety Reuse.
ICPC
Sergio Areias, Daniela Carneiro da Cruz, Jorge Sousa Pinto
2010 — conf
Contract-Based Slicing.
ISoLA (1)
Daniela Carneiro da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto
2010 J jnl
Deductive verification of cryptographic software.
Innov. Syst. Softw. Eng.
José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira
2010 — conf
GamaSlicer: an online laboratory for program verification and analysis.
LDTA
Daniela Carneiro da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto
2010 — conf
Model-Checking Temporal Properties of Real-Time HTL Programs.
ISoLA (2)
André Carvalho, Joel Carvalho, Jorge Sousa Pinto, Simão Melo de Sousa
2010 Misc conf
Program Verification in SPARK and ACSL: A Comparative Case Study.
Ada-Europe
Eduardo Brito, Jorge Sousa Pinto
2010 J jnl
Safe Integration of Annotated Components in Open Source Projects.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Sergio Areias, Daniela Carneiro da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto
2009 — conf
Deductive Verification of Cryptographic Software.
NASA Formal Methods
Manuel Barbosa, José Bacelar Almeida, Jorge Sousa Pinto, Bárbara Vieira
2009 J jnl
Iterators, Recursors and Interaction Nets
CoRR
Ian Mackie, Jorge Sousa Pinto, Miguel Vilaça
2009 — ed.
Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised Tutorial Lectures
LerNet ALFA Summer School
Ana Bove, Luís Soares Barbosa, Alberto Pardo, Jorge Sousa Pinto
2009 C conf
Verifying Cryptographic Software Correctness with Respect to Reference Implementations.
FMICS
José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira
2008 J jnl
Deriving Sorting Algorithms
CoRR
José Bacelar Almeida, Jorge Sousa Pinto
2008 J jnl
Lissom, a Source Level Proof Carrying Code Platform
CoRR
João Gomes, Daniel Martins, Simão Melo de Sousa, Jorge Sousa Pinto
2008 — conf
Preface.
RULE
Günter Kniesel, Jorge Sousa Pinto
2008 C conf
Visual Programming with Interaction Nets.
Diagrams
Abubakar Hassan, Ian Mackie, Jorge Sousa Pinto
2007 — conf
A Tool for Programming with Interaction Nets.
RULE@RDP
José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça
2007 — conf
Token-passing Nets for Functional Languages.
WRS@RDP
José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça
2007 J jnl
Visual Programming with Recursion Patterns in Interaction Nets.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Ian Mackie, Jorge Sousa Pinto, Miguel Vilaça
2006 — conf
A Local Graph-rewriting System for Deciding Equality in Sum-product Theories.
TERMGRAPH@ETAPS
José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça
2005 — conf
A Framework for Point-Free Program Transformation.
IFL
Alcino Cunha, Jorge Sousa Pinto, José Proença
2005 J jnl
Point-free Program Transformation.
Fundam. Informaticae
Alcino Cunha, Jorge Sousa Pinto
2005 J jnl
Recursion patterns and time-analysis.
ACM SIGPLAN Notices
Manuel Barbosa, Alcino Cunha, Jorge Sousa Pinto
2003 — conf
Weak reduction and garbage collection in interaction nets.
WRS
Jorge Sousa Pinto
2002 — conf
A Higher-Order Calculus for Graph Transformation.
TERMGRAPH
Maribel Fernández, Ian Mackie, Jorge Sousa Pinto
2002 J jnl
Encoding Linear Logic with Interaction Combinators.
Inf. Comput.
Ian Mackie, Jorge Sousa Pinto
2001 — conf
Combining interaction nets with externally defined programs.
APPIA-GULP-PRODE
Maribel Fernández, Ian Mackie, Jorge Sousa Pinto
2001 — conf
Parallel Evaluation of Interaction Nets with MPINE.
RTA
Jorge Sousa Pinto
2001 — conf
Parallel Implementation Models for the lambda-Calculus Using the Geometry of Interaction.
TLCA
Jorge Sousa Pinto
2000 B conf
Sequential and Concurrent Abstract Machines for Interaction Nets.
FoSSaCS
Jorge Sousa Pinto
1996 B conf
Using Internet technology for course support.
ITiCSE
José Eduardo Pina Miranda, Jorge Sousa Pinto