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 (preprint)
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, S. Feder, J. Kukovec, A. Kupriyanov, G. Moreira, P. Offtermatt, T. Pani, T. Tran, and I. Konnov. The TLA+ Model Checker Apalache. 38th International Conference on Computer-Aided Verification (CAV'26). To Appear
2. A. Becchi, M. Blicha, R. Otoni, and N. Sharygina. PyCHC: a Framework for Modelling and Certified Solving of CHC Systems. 38th International Conference on Computer-Aided Verification (CAV'26). To Appear
3. Y. Wang, R. Álvarez, C. Tirelli, R. Otoni, G. Ansaloni, L. Pozzi, and D. Atienza. FACETs: Fast and Efficient Compilation for Control–Dataflow Mapping on CGRAs. 22nd International Symposium on Applied Reconfigurable Computing (ARC'26). To Appear
   Best Paper Award
4. 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
5. 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
6. 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
7. 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
8. 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
9. 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
10. 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. A. Buccolini, M. Biasion, R. Otoni, G. Constantinides, and L. Pozzi. Towards Input-Distribution-Aware Approximate Multiplier Generation for CNNs. 29th Design, Automation and Test in Europe Conference (DATE'26) – Extended Abstract. To Appear
2. R. Otoni. Automatisierte Garantierte Blockchain-Technologie Verifizierung. GI Ausgezeichnete Informatikdissertationen 2023 (Band 24), 2024. DOI
3. A. Buckley, P. Chuprikov, R. Otoni, R. Rand, R. Soulé, and P. Eugster. Towards an Algebraic Specification of Quantum Networks. 1st Workshop on Quantum Networks and Distributed Quantum Computing (QuNet'23). DOI