Jorge Sousa Pinto

Publication Activity (10 Years)

Years Active: 1996-2023
Publications (10 Years): 14

Top Topics

Imperative Programs

Software Implementation

Automata Theoretic

Top Venues

J. Log. Algebraic Methods Program.

Sci. Comput. Program.

Publications

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