Journal Papers

1. M. Rezaalipour, M. Biasion, F. Costa, C. Tirelli, L. Ferretti, R. Otoni, G. Constantinides, and L. Pozzi. Approximate Logic Synthesis via Iterative SMT-based Subcircuit Rewriting. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), Early Access. DOI
2. A. Buckley, P. Chuprikov, R. Otoni, R. Soulé, R. Rand, and P. Eugster. A Language for Quantifying Quantum Network Behavior. Proceedings of the ACM on Programming Languages (PACMPL), 9(OOPSLA2), 2025. DOI
3. R. Otoni, M. Blicha, P. Eugster, and N. Sharygina. Validation of CHC Satisfiability with ATHENA. Formal Aspects of Computing (FAC), 37(4), 2025. DOI
4. A. Buckley, P. Chuprikov, R. Otoni, R. Soulé, R. Rand, and P. Eugster. An Algebraic Language for Specifying Quantum Networks. Proceedings of the ACM on Programming Languages (PACMPL), 8(PLDI), 2024. DOI
5. R. Otoni, M. Marescotti, L. Alt, P. Eugster, A. Hyvärinen, and N. Sharygina. A Solicitous Approach to Smart Contract Verification. ACM Transactions on Privacy and Security (TOPS), 26(2), 2023. DOI

Conference Papers

1. R. Otoni, M. Blicha, M. Rivera, P. Eugster, J. Kofroň, and N. Sharygina. Unsatisfiability Proofs for Horn Solving. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'25). DOI
   Distinguished Paper Award and EASST Best Paper Award
2. C. Tirelli, R. Otoni, and L. Pozzi. Monomorphism-based CGRA Mapping via Space and Time Decoupling. 28th Design, Automation and Test in Europe Conference (DATE'25). DOI
3. R. Otoni, M. Blicha, P. Eugster, and N. Sharygina. CHC Model Validation with Proof Guarantees. 18th International Conference on integrated Formal Methods (iFM'23). DOI
   Best Paper Award candidate
4. R. Otoni, I. Konnov, J. Kukovec, P. Eugster, and N. Sharygina. Symbolic Model Checking for TLA+ Made Faster. 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23). DOI
5. R. Otoni, M. Blicha, P. Eugster, A. Hyvärinen, and N. Sharygina. Theory-Specific Proof Steps Witnessing Correctness of SMT Executions. 58th ACM/IEEE Design Automation Conference (DAC'21). DOI
6. M. Marescotti, R. Otoni, L. Alt, P. Eugster, A. Hyvärinen, and N. Sharygina. Accurate Smart Contract Verification Through Direct Modelling. 9th International Symposium on Leveraging Applications of Formal Methods (ISoLA'20). DOI
7. R. Otoni, A. Cavalcanti, and A. Sampaio. Local Analysis of Determinism for CSP. 20th Brazilian Symposium on Formal Methods (SBMF'17). DOI

Other Papers

1. R. Otoni. Automatisierte Garantierte Blockchain-Technologie Verifizierung. GI Ausgezeichnete Informatikdissertationen 2023 (Band 24), 2024. DOI
2. A. Buckley, P. Chuprikov, R. Otoni, R. Soulé, R. Rand, and P. Eugster. Towards an Algebraic Specification of Quantum Networks. 1st Workshop on Quantum Networks and Distributed Quantum Computing (QuNet'23). DOI