Jorge Sousa Pinto

J. Log. Algebraic Methods Program., June, 2023

2022

A tribute to José Manuel Valença.

[BibT_eX]

[DOI]

José Nuno Oliveira

Luís Soares Barbosa

J. Log. Algebraic Methods Program., 2022

Why3-do: The Way of Harmonious Distributed System Proofs.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2022

2021

A deductive reasoning approach for database applications using verification conditions.

[BibT_eX]

[DOI]

Md. Imran Alam

Raju Halder

J. Syst. Softw., 2021

2020

Real-time MTL with durations as SMT with applications to schedulability analysis.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Theoretical Aspects of Software Engineering, 2020

Testing for Race Conditions in Distributed Systems via SMT Solving.

[BibT_eX]

[DOI]

João Carlos Pereira

Nuno Machado

Proceedings of the Tests and Proofs - 14th International Conference, 2020

2019

A generalized program verification workflow based on loop elimination and SA form.

[BibT_eX]

[DOI]

Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, 2019

2018

Runtime verification of autopilot systems using a fragment of MTL- $${\int }$$ ∫.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2018

K-Taint: An Executable Rewriting Logic Semantics for Taint Analysis in the K Framework.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering, 2018

A Generalized Approach to Verification Condition Generation.

[BibT_eX]

[DOI]

Shin Nakajima

Rovedy Aparecida Busquim e Silva

Proceedings of the 2018 IEEE 42nd Annual Computer Software and Applications Conference, 2018

2017

SMT-based schedulability analysis using RMTL-∫.

[BibT_eX]

[DOI]

SIGBED Rev., 2017

2016

Formal Verification With Frama-C: A Case Study in the Space Software Domain.

[BibT_eX]

[DOI]

Nanci Naomi Arai

Luciana Akemi Burgareli

José Maria Parente de Oliveira

IEEE Trans. Reliab., 2016

A Single-Assignment Translation for Annotated Programs.

[BibT_eX]

[DOI]

CoRR, 2016

Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2016

2015

Logic-based schedulability analysis for compositional hard real-time embedded systems.

[BibT_eX]

[DOI]

SIGBED Rev., 2015

Studying Verification Conditions for Imperative Programs.

[BibT_eX]

[DOI]

Si-Mohamed Lamraoui

Shin Nakajima

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2015

Monitoring for a Decidable Fragment of MTL-∫.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 6th International Conference, 2015

2014

CAOVerif: An open-source deductive verification platform for cryptographic software implementations.

[BibT_eX]

[DOI]

Jean-Christophe Filliâtre

Manuel Barbosa

Bárbara Vieira

Sci. Comput. Program., 2014

A Compositional Monitoring Framework for Hard Real-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

Formal Verification of kLIBC with the WP Frama-C Plug-in.

[BibT_eX]

[DOI]

Nuno Carvalho

Cristiano da Silva Sousa

Aaron Tomb

Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

A Bounded Model Checker for SPARK Programs.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2014

Towards a Runtime Verification Framework for the Ada Programming Language.

[BibT_eX]

[DOI]

Proceedings of the Reliable Software Technologies, 2014

2013

Formal verification of side-channel countermeasures using self-composition.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2013

Interactive Verification of Safety-Critical Software.

[BibT_eX]

[DOI]

Proceedings of the 37th Annual IEEE Computer Software and Applications Conference, 2013

Towards a mostly-automated prover for bit-vector arithmetic.

[BibT_eX]

[DOI]

Iago Abal

Proceedings of the International C* Conference on Computer Science & Software Engineering, 2013

2012

Assertion-based slicing and slice graphs.

[BibT_eX]

[DOI]

José Bernardo Barros

Formal Aspects Comput., 2012

Using Term Rewriting to Solve Bit-Vector Arithmetic Problems - (Poster Presentation).

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Verification conditions for single-assignment programs.

[BibT_eX]

[DOI]

Proceedings of the ACM Symposium on Applied Computing, 2012

An Approach to Model Checking Ada Programs.

[BibT_eX]

[DOI]

José Miguel Faria

João Martins

Proceedings of the Reliable Software Technologies - Ada-Europe 2012, 2012

2011

Rigorous Software Development - An Introduction to Program Verification.

[BibT_eX]

[DOI]

Undergraduate Topics in Computer Science, Springer, ISBN: 978-0-85729-018-2, 2011

Verification conditions for source-level imperative programs.

[BibT_eX]

[DOI]

Comput. Sci. Rev., 2011

GammaPolarSlicer.

[BibT_eX]

[DOI]

Sergio Areias

Comput. Sci. Inf. Syst., 2011

2010

Deductive verification of cryptographic software.

[BibT_eX]

[DOI]

Innov. Syst. Softw. Eng., 2010

A Deductive Verification Platform for Cryptographic Software.

[BibT_eX]

[DOI]

Manuel Barbosa

Jean-Christophe Filliâtre

Bárbara Vieira

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010

Safe Integration of Annotated Components in Open Source Projects.

[BibT_eX]

[DOI]

Sergio Areias

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010

GamaSlicer: an online laboratory for program verification and analysis.

[BibT_eX]

[DOI]

Proceedings of the of the Tenth Workshop on Language Descriptions, Tools and Applications, 2010

Contract-Based Slicing Helps on Safety Reuse.

[BibT_eX]

[DOI]

Sergio Areias

Proceedings of the 18th IEEE International Conference on Program Comprehension, 2010

Contract-Based Slicing.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010

Model-Checking Temporal Properties of Real-Time HTL Programs.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010

Program Verification in SPARK and ACSL: A Comparative Case Study.

[BibT_eX]

[DOI]

Eduardo Brito

Proceedings of the Reliable Software Technologiey, 2010

2009

Iterators, Recursors and Interaction Nets

[BibT_eX]

[DOI]

CoRR, 2009

Verifying Cryptographic Software Correctness with Respect to Reference Implementations.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2009

2008

Preface.

[BibT_eX]

[DOI]

Günter Kniesel

Proceedings of the Ninth International Workshop on Rule-Based Programming, 2008

Lissom, a Source Level Proof Carrying Code Platform

[BibT_eX]

[DOI]

CoRR, 2008

Deriving Sorting Algorithms

[BibT_eX]

[DOI]

CoRR, 2008

Visual Programming with Interaction Nets.

[BibT_eX]

[DOI]

Abubakar Hassan

Proceedings of the Diagrammatic Representation and Inference, 5th International Conference, 2008

2007

A Tool for Programming with Interaction Nets.

[BibT_eX]

[DOI]

Proceedings of the Eighth International Workshop on Rule Based Programming, 2007

Token-passing Nets for Functional Languages.

[BibT_eX]

[DOI]

Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming, 2007

Visual Programming with Recursion Patterns in Interaction Nets.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2007

2006

A Local Graph-rewriting System for Deciding Equality in Sum-product Theories.

[BibT_eX]

[DOI]

Proceedings of the Third International Workshop on Term Graph Rewriting, 2006

2005

Recursion patterns and time-analysis.

[BibT_eX]

[DOI]

Manuel Barbosa

Alcino Cunha

ACM SIGPLAN Notices, 2005

Point-free Program Transformation.

[BibT_eX]

[DOI]

Alcino Cunha

Fundam. Informaticae, 2005

A Framework for Point-Free Program Transformation.

[BibT_eX]

[DOI]

Alcino Cunha

José Proença

Proceedings of the Implementation and Application of Functional Languages, 2005

2003

Weak reduction and garbage collection in interaction nets.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Workshop on Reduction Strategies in Rewriting and Programming, 2003

2002

Encoding Linear Logic with Interaction Combinators.

[BibT_eX]

[DOI]

Inf. Comput., 2002

A Higher-Order Calculus for Graph Transformation.

[BibT_eX]

[DOI]

Maribel Fernández

Proceedings of the First International Workshop on Term Graph Rewriting, 2002

2001

Parallel Implementation Models for the lambda-Calculus Using the Geometry of Interaction.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

Parallel Evaluation of Interaction Nets with MPINE.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 12th International Conference, 2001

Combining interaction nets with externally defined programs.

[BibT_eX]

[DOI]

Maribel Fernández

Proceedings of the APPIA-GULP-PRODE 2001: Joint Conference on Declarative Programming, 2001

2000

Sequential and Concurrent Abstract Machines for Interaction Nets.

[BibT_eX]

[DOI]

José Eduardo Pina Miranda

Proceedings of the Foundations of Software Science and Computation Structures, 2000

1996

Using Internet technology for course support.

[BibT_eX]

[DOI]