Local Analysis of Determinism for CSP. - Rodrigo Otoni; Ana Cavalcanti 001; Augusto Sampaio 001 (SBMF, 2017)

Accurate Smart Contract Verification Through Direct Modelling. - Matteo Marescotti; Rodrigo Otoni; Leonardo Alt; Patrick Eugster; Antti E. J. Hyvärinen; Natasha Sharygina (ISoLA (3), 2020)

Theory-Specific Proof Steps Witnessing Correctness of SMT Executions. - Rodrigo Otoni; Martin Blicha; Patrick Eugster; Antti E. J. Hyvärinen; Natasha Sharygina (DAC, 2021)

CHC Model Validation with Proof Guarantees. - Rodrigo Otoni; Martin Blicha; Patrick Eugster; Natasha Sharygina (iFM, 2023)

Towards an Algebraic Specification of Quantum Networks. - Anita Buckley; Pavel Chuprikov; Rodrigo Otoni; Robert Rand 001; Robert Soulé; Patrick Eugster (QuNet@SIGCOMM, 2023)

Symbolic Model Checking for TLA+ Made Faster. - Rodrigo Otoni; Igor Konnov 001; Jure Kukovec; Patrick Eugster; Natasha Sharygina (TACAS (1), 2023)

Automatisierte Garantierte Blockchain-Technologie Verifizierung. - Rodrigo Otoni (Ausgezeichnete Informatikdissertationen, 2023)

A Solicitous Approach to Smart Contract Verification. - Rodrigo Otoni; Matteo Marescotti; Leonardo Alt; Patrick Eugster; Antti E. J. Hyvärinen; Natasha Sharygina (ACM Trans. Priv. Secur., 2023)

An Algebraic Language for Specifying Quantum Networks. - Anita Buckley; Pavel Chuprikov; Rodrigo Otoni; Robert Soulé; Robert Rand 001; Patrick Eugster (Proc. ACM Program. Lang., 2024)

Monomorphism-Based CGRA Mapping Via Space and Time Decoupling. - Cristian Tirelli; Rodrigo Otoni; Laura Pozzi 001 (DATE, 2025)

Unsatisfiability Proofs for Horn Solving. - Rodrigo Otoni; Martin Blicha; Matias Barandiaran Rivera; Patrick Eugster; Jan Kofron; Natasha Sharygina (TACAS (2), 2025)

Artifact for the paper Unsatisfiability Proofs for Horn Solving. - Rodrigo Otoni; Martin Blicha; Matias Barandiaran Rivera; Patrick Eugster; Jan Kofron; Natasha Sharygina (Zenodo, 2025)