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

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)

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

A framework for quality assessment of ROS repositories. - André Santos 001; Alcino Cunha; Nuno Macedo 001; Cláudio Lourenço (IROS, 2016)

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

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)

Single-assignment program verification - Cláudio Belo Lourenço (2018)

GOSPEL - Providing OCaml with a Formal Specification Language. - Arthur Charguéraud; Jean-Christophe Filliâtre; Cláudio Lourenço; Mário Pereira (FM, 2019)

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)

Automated Verification of Temporal Properties of Ladder Programs. - Cláudio Belo Lourenço; Denis Cousineau 002; Florian Faissole; Claude Marché; David Mentré; Hiroaki Inoue (FMICS, 2021)

Explaining Counterexamples with Giant-Step Assertion Checking. - Benedikt F. H. Becker; Cláudio Belo Lourenço; Claude Marché (F-IDE@NFM, 2021)

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

Automated formal analysis of temporal properties of Ladder programs. - Cláudio Belo Lourenço; Denis Cousineau 002; Florian Faissole; Claude Marché; David Mentré; Hiroaki Inoue (Int. J. Softw. Tools Technol. Transf., 2022)

Closure Conversion, Flat Environments, and the Complexity of Abstract Machines. - Beniamino Accattoli; Dan Ghica; Giulio Guerrieri; Cláudio Belo Lourenço; Claudio Sacerdoti Coen (CoRR, 2025)

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