Pedro Antonino

28 papers A 1B 3Misc 1Journal 17Unranked 6
YearRankTypeTitle / Venue / Authors
2026 J jnl
Formally Verifying Noir Zero Knowledge Programs with NAVe.
CoRR
Pedro Antonino, Namrata Jain
2026 J jnl
Generating formal smart-contract specifications: comparing few-shot learning and fine-tuned LLMs.
Sci. Comput. Program.
Gabriel Leite, Filipe Arruda, Pedro Antonino, Augusto Sampaio, A. W. Roscoe
2025 J jnl
Demystification and Near-perfect Estimation of Minimum Gas Limit and Gas Used for Ethereum Smart Contracts.
CoRR
Danilo Rafael de Lima Cabral, Pedro Antonino, Augusto Sampaio
2025 J jnl
Demystification and near-perfect estimation of minimum gas limit and gas used for Ethereum smart contracts.
J. Cloud Comput.
Danilo Rafael de Lima Cabral, Pedro Antonino, Augusto Cezar Alves Sampaio
2025 A conf
Hierarchical Consensus: Scalability Through Optimism and Weak Liveness.
DISC
Pedro Antonino, Antoine Durand, A. W. Roscoe
2024 J jnl
A formal component model for UML based on CSP aiming at compositional verification.
Softw. Syst. Model.
Flávia Falcão, Lucas Lima, Augusto Sampaio, Pedro Antonino
2024 J jnl
A refinement-based approach to safe smart contract deployment and evolution.
Softw. Syst. Model.
Pedro Antonino, Juliandson Ferreira, Augusto Sampaio, A. W. Roscoe, Filipe Arruda
2024 — conf
Abstracting and Verifying Decentralised Systems in CSP.
The Application of Formal Methods
A. W. Roscoe, Pedro Antonino, Jonathan Lawrence
2024 — conf
Extracting Formal Smart-Contract Specifications from Natural Language with LLMs.
FACS
Gabriel Leite, Filipe Arruda, Pedro Antonino, Augusto Sampaio, A. W. Roscoe
2024 B conf
Hooks: A Simple and Modular Checkpointing Protocol for Blockchains.
NCA
Pedro Antonino, Antoine Durand, Namrata Jain, Garry Lancaster, Jonathan Lawrence, A. W. Roscoe
2024 — conf
Trusted Deployer: A Tool for Safe Creation and Upgrade of Ethereum Smart Contracts.
SBMF
Juliandson Ferreira, Pedro Antonino, Augusto Sampaio, A. W. Roscoe, Filipe Arruda
2023 J jnl
Flexible Remote Attestation of Pre-SNP SEV VMs Using SGX Enclaves.
IEEE Access
Pedro Antonino, Ante Derek, Wojciech Aleksander Woloszyn
2023 J jnl
Flexible remote attestation of pre-SNP SEV VMs using SGX enclaves.
CoRR
Pedro Antonino, Ante Derek, Wojciech Aleksander Woloszyn
2023 — conf
The Consensus Machine: Formalising Consensus in the Presence of Malign Agents.
Theories of Programming and Formal Methods
A. W. Roscoe, Pedro Antonino, Jonathan Lawrence
2022 J jnl
A Pattern-based deadlock-freedom analysis strategy for concurrent systems.
CoRR
Pedro Antonino, Augusto Sampaio, Jim Woodcock
2022 J jnl
Approximate verification of concurrent systems using token structures and invariants.
Int. J. Softw. Tools Technol. Transf.
Pedro Antonino, Thomas Gibson-Robinson, A. W. Roscoe
2022 B conf
Specification is Law: Safe Creation and Upgrade of Ethereum Smart Contracts.
SEFM
Pedro Antonino, Juliandson Ferreira, Augusto Sampaio, A. W. Roscoe
2022 J jnl
Specification is Law: Safe Creation and Upgrade of Ethereum Smart Contracts.
CoRR
Pedro Antonino, Juliandson Ferreira, Augusto Sampaio, A. W. Roscoe
2021 — conf
Guardian: Symbolic Validation of Orderliness in SGX Enclaves.
CCSW
Pedro Antonino, Wojciech Aleksander Woloszyn, A. W. Roscoe
2021 J jnl
Guardian: symbolic validation of orderliness in SGX enclaves.
CoRR
Pedro Antonino, Wojciech Aleksander Woloszyn, A. W. Roscoe
2021 Misc conf
Solidifier: bounded model checking solidity using lazy contract deployment and precise memory modelling.
SAC
Pedro Antonino, A. W. Roscoe
2021 J jnl
Trusted And Confidential Program Analysis.
CoRR
Han Liu, Pedro Antonino, Zhiqiang Yang, Chao Liu, A. W. Roscoe
2020 J jnl
Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity.
CoRR
Pedro Antonino, A. W. Roscoe
2019 J jnl
Efficient Verification of Concurrent Systems Using Synchronisation Analysis and SAT/SMT Solving.
ACM Trans. Softw. Eng. Methodol.
Pedro Antonino, Thomas Gibson-Robinson, A. W. Roscoe
2019 J jnl
Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving.
Formal Aspects Comput.
Pedro Antonino, Thomas Gibson-Robinson, A. W. Roscoe
2017 — conf
Checking Static Properties Using Conservative SAT Approximations for Reachability.
SBMF
Pedro Antonino, Thomas Gibson-Robinson, A. W. Roscoe
2016 B conf
Efficient Deadlock-Freedom Checking Using Local Analysis and SAT Solving.
IFM
Pedro Antonino, Thomas Gibson-Robinson, A. W. Roscoe
2016 J jnl
Rigorous development of component-based systems using component metadata and patterns.
Formal Aspects Comput.
Marcel Vinícius Medeiros Oliveira, Pedro Antonino, Rodrigo Ramos, Augusto Sampaio, Alexandre Cabral Mota, A. W. Roscoe