Algebraic Laws for Process Subtyping. - José Dihego; Pedro R. G. Antonino; Augusto Sampaio 001 (ICFEM, 2013)

A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes. - Pedro R. G. Antonino; Augusto Sampaio 001; Jim Woodcock 001 (FM, 2014)

Leadership Election: An Industrial SoS Application of Compositional Deadlock Verification. - Pedro R. G. Antonino; Marcel Vinícius Medeiros Oliveira; Augusto Sampaio 001; Klaus E. Kristensen; Jeremy W. Bryans (NASA Formal Methods, 2014)

Tighter Reachability Criteria for Deadlock-Freedom Analysis. - Pedro R. G. Antonino; Thomas Gibson-Robinson; A. W. Roscoe 001 (FM, 2016)

Efficient Deadlock-Freedom Checking Using Local Analysis and SAT Solving. - Pedro Antonino; Thomas Gibson-Robinson; A. W. Roscoe 001 (IFM, 2016)

Rigorous development of component-based systems using component metadata and patterns. - Marcel Vinícius Medeiros Oliveira; Pedro Antonino; Rodrigo Ramos; Augusto Sampaio 001; Alexandre Cabral Mota; A. W. Roscoe 001 (Formal Aspects Comput., 2016)

Checking Static Properties Using Conservative SAT Approximations for Reachability. - Pedro Antonino; Thomas Gibson-Robinson; A. W. Roscoe 001 (SBMF, 2017)

The Automatic Detection of Token Structures and Invariants Using SAT Checking. - Pedro R. G. Antonino; Thomas Gibson-Robinson; A. W. Roscoe 001 (TACAS (2), 2017)

Verifying concurrent systems by approximation. - Pedro Ribeiro Gonçalves Antonino (2018)

Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving. - Pedro Antonino; Thomas Gibson-Robinson; A. W. Roscoe 001 (Formal Aspects Comput., 2019)

Efficient Verification of Concurrent Systems Using Synchronisation Analysis and SAT/SMT Solving. - Pedro Antonino; Thomas Gibson-Robinson; A. W. Roscoe 001 (ACM Trans. Softw. Eng. Methodol., 2019)

Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity. - Pedro Antonino; A. W. Roscoe 001 (CoRR, 2020)

Guardian: Symbolic Validation of Orderliness in SGX Enclaves. - Pedro Antonino; Wojciech Aleksander Woloszyn; A. W. Roscoe 001 (CCSW, 2021)

Solidifier: bounded model checking solidity using lazy contract deployment and precise memory modelling. - Pedro Antonino; A. W. Roscoe 001 (SAC, 2021)

Trusted And Confidential Program Analysis. - Han Liu 010; Pedro Antonino; Zhiqiang Yang; Chao Liu 032; A. W. Roscoe 001 (CoRR, 2021)

Specification is Law: Safe Creation and Upgrade of Ethereum Smart Contracts. - Pedro Antonino; Juliandson Ferreira; Augusto Sampaio 001; A. W. Roscoe 001 (SEFM, 2022)

A Pattern-based deadlock-freedom analysis strategy for concurrent systems. - Pedro Antonino; Augusto Sampaio 001; Jim Woodcock 001 (CoRR, 2022)

Approximate verification of concurrent systems using token structures and invariants. - Pedro Antonino; Thomas Gibson-Robinson; A. W. Roscoe 001 (Int. J. Softw. Tools Technol. Transf., 2022)

The Consensus Machine: Formalising Consensus in the Presence of Malign Agents. - A. W. Roscoe 001; Pedro Antonino; Jonathan Lawrence (Theories of Programming and Formal Methods, 2023)

Flexible Remote Attestation of Pre-SNP SEV VMs Using SGX Enclaves. - Pedro Antonino; Ante Derek; Wojciech Aleksander Woloszyn (IEEE Access, 2023)

Abstracting and Verifying Decentralised Systems in CSP. - A. W. Roscoe 001; Pedro Antonino; Jonathan Lawrence (The Application of Formal Methods, 2024)

Extracting Formal Smart-Contract Specifications from Natural Language with LLMs. - Gabriel Leite; Filipe Arruda; Pedro Antonino; Augusto Sampaio 001; A. W. Roscoe 001 (FACS, 2024)

Hooks: A Simple and Modular Checkpointing Protocol for Blockchains. - Pedro Antonino; Antoine Durand; Namrata Jain; Garry Lancaster; Jonathan Lawrence; A. W. Roscoe 001 (NCA, 2024)

Trusted Deployer: A Tool for Safe Creation and Upgrade of Ethereum Smart Contracts. - Juliandson Ferreira; Pedro Antonino; Augusto Sampaio 001; A. W. Roscoe 001; Filipe Arruda (SBMF, 2024)

A refinement-based approach to safe smart contract deployment and evolution. - Pedro Antonino; Juliandson Ferreira; Augusto Sampaio 001; A. W. Roscoe 001; Filipe Arruda (Softw. Syst. Model., 2024)

A formal component model for UML based on CSP aiming at compositional verification. - Flávia Falcão; Lucas Lima 001; Augusto Sampaio 001; Pedro Antonino (Softw. Syst. Model., 2024)

Demystification and near-perfect estimation of minimum gas limit and gas used for Ethereum smart contracts. - Danilo Rafael de Lima Cabral; Pedro Antonino; Augusto Cezar Alves Sampaio (J. Cloud Comput., 2025)