Cláudio Belo Lourenço
Cláudio Belo Lourenço
Huawei Central Software Institute (UK)
Verified email at
Cited by
Cited by
A framework for quality assessment of ROS repositories
A Santos, A Cunha, N Macedo, C Lourenço
Intelligent Robots and Systems (IROS), 2016 IEEE/RSJ International …, 2016
GOSPEL—providing OCaml with a formal specification language
A Charguéraud, JC Filliâtre, C Lourenço, M Pereira
Formal Methods–The Next 30 Years: Third World Congress, FM 2019, Porto …, 2019
Explaining Counterexamples with Giant-Step Assertion Checking
B Becker, C Lourenço, C Marché
F-IDE 2021-6th Workshop on Formal Integrated Development Environments, 2021
Studying Verification Conditions for Imperative Programs
CB Lourenço, SM Lamraoui, S Nakajima, JS Pinto
15th International Workshop on Automated Verification of Critical Systems 72, 2015
Formalizing single-assignment program verification: An adaptation-complete approach
C Belo Lourenço, MJ Frade, J Sousa Pinto
Programming Languages and Systems: 25th European Symposium on Programming …, 2016
A generalized program verification workflow based on loop elimination and SA form
CB Lourenço, MJ Frade, JS Pinto
2019 IEEE/ACM 7th International Conference on Formal Methods in Software …, 2019
A bounded model checker for SPARK programs
CB Lourenço, MJ Frade, JS Pinto
Automated Technology for Verification and Analysis: 12th International …, 2014
A bounded model checker for SPARK programs
CB Lourenço
Master’s thesis, University of Minho, 2013
Automated formal analysis of temporal properties of ladder programs
C Belo Lourenço, D Cousineau, F Faissole, C Marché, D Mentré, H Inoue
International Journal on Software Tools for Technology Transfer 24 (6), 977-997, 2022
Single-assignment program verification
CFBS Lourenço
Why3-do: The Way of Harmonious Distributed System Proofs
CB Lourenço, JS Pinto
European Symposium on Programming, 114-142, 2022
Automated Verification of Temporal Properties of Ladder Programs
CB Lourenço, D Cousineau, F Faissole, C Marché, D Mentré, H Inoue
International Conference on Formal Methods for Industrial Critical Systems …, 2021
A toolchain to produce verified OCaml libraries
JC Filliâtre, L Gondelman, C Lourenço, A Paskevich, M Pereira, ...
Research report, Université Paris-Saclay, 2020
A Generalized Approach to Verification Condition Generation
CB Lourenço, MJ Frade, S Nakajima, JS Pinto
2018 IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC …, 2018
Giant-step Semantics for the Categorisation of Counterexamples
B Becker, CB Lourenço, C Marché
Inria, 2021
A Tutorial on Verification Conditions Using Single-Assignment Form
CB Lourenço, MJ Frade, JS Pinto
unpublished draft available from http://haslab. uminho. pt/jsp), University …, 2015
Experimenting with predicate abstraction
VC Miraldo, MJ Frade, C Lourenço, JS Pinto
Formal Analysis of Ladder Programs using Deductive Verification
C Lourenço, D Cousineau, F Faissole, C Marché, D Mentré, H Inoue
Inria, 2021
You-Know-Why: an Early-Stage Prototype of a Key Server Developed using Why3
D Diverio, C Lourenço, C Marché
VerifyThis 2020-Long-term Challenge, 4--7, 2020
A Single-Assignment Translation for Annotated Programs
CB Lourenço, MJ Frade, JS Pinto
arXiv preprint arXiv:1601.00584, 2016
The system can't perform the operation now. Try again later.
Articles 1–20