1919M. Rezaalipour, M. Biasion, F. Costa, C. Tirelli, L. Ferretti, <ins >R. Otoni</ins >, G. Constantinides, and L. Pozzi.
2020<b >Approximate Logic Synthesis via Iterative SMT-based Subcircuit Rewriting</b >.
2121IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), Early Access.
22- <a href =" https://doi.org/10.1109/TCAD.2025.3638267 " >DOI</a > (<a href =" https://rodrigo7491.github.io/files/papers/Approximate_Logic_Synthesis_via_Iterative_SMT-based_Subcircuit_Rewriting.pdf " >preprint</a >)
22+ <a href =" https://doi.org/10.1109/TCAD.2025.3638267 " >DOI</a >
23+ (<a href =" https://rodrigo7491.github.io/files/papers/Approximate_Logic_Synthesis_via_Iterative_SMT-based_Subcircuit_Rewriting.pdf " >preprint</a >)
2324</li >
2425
2526<li >
2627A. Buckley, P. Chuprikov, <ins >R. Otoni</ins >, R. Soulé, R. Rand, and P. Eugster.
2728<b >A Language for Quantifying Quantum Network Behavior</b >.
2829Proceedings of the ACM on Programming Languages (PACMPL), 9(OOPSLA2), 2025.
2930<a href =" https://doi.org/10.1145/3763135 " >DOI</a >
31+ (open access)
3032</li >
3133
3234<li >
3335<ins >R. Otoni</ins >, M. Blicha, P. Eugster, and N. Sharygina.
3436<b >Validation of CHC Satisfiability with ATHENA</b >.
3537Formal Aspects of Computing (FAC), 37(4), 2025.
3638<a href =" https://doi.org/10.1145/3716505 " >DOI</a >
39+ (open access)
3740</li >
3841
3942<li >
4043A. Buckley, P. Chuprikov, <ins >R. Otoni</ins >, R. Soulé, R. Rand, and P. Eugster.
4144<b >An Algebraic Language for Specifying Quantum Networks</b >.
4245Proceedings of the ACM on Programming Languages (PACMPL), 8(PLDI), 2024.
4346<a href =" https://doi.org/10.1145/3656430 " >DOI</a >
47+ (open access)
4448</li >
4549
4650<li >
4751<ins >R. Otoni</ins >, M. Marescotti, L. Alt, P. Eugster, A. Hyvärinen, and N. Sharygina.
4852<b >A Solicitous Approach to Smart Contract Verification</b >.
4953ACM Transactions on Privacy and Security (TOPS), 26(2), 2023.
5054<a href =" https://doi.org/10.1145/3564699 " >DOI</a >
55+ (open access)
5156</li >
5257
5358</ol >
@@ -84,6 +89,7 @@ Y. Wang, R. Álvarez, C. Tirelli, <ins>R. Otoni</ins>, G. Ansaloni, L. Pozzi, an
8489<b >Unsatisfiability Proofs for Horn Solving</b >.
859031st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'25).
8691<a href =" https://doi.org/10.1007/978-3-031-90653-4_4 " >DOI</a >
92+ (open access)
8793<br >
8894<i >Distinguished Paper Award</i > and <i >EASST Best Paper Award</i >
8995</li >
@@ -93,13 +99,15 @@ C. Tirelli, <ins>R. Otoni</ins>, and L. Pozzi.
9399<b >Monomorphism-based CGRA Mapping via Space and Time Decoupling</b >.
9410028th Design, Automation and Test in Europe Conference (DATE'25).
95101<a href =" https://doi.org/10.23919/DATE64628.2025.10992940 " >DOI</a >
102+ (<a href =" https://doi.org/10.48550/arXiv.2512.02859 " >arXiv</a >)
96103</li >
97104
98105<li >
99106<ins >R. Otoni</ins >, M. Blicha, P. Eugster, and N. Sharygina.
100107<b >CHC Model Validation with Proof Guarantees</b >.
10110818th International Conference on integrated Formal Methods (iFM'23).
102109<a href =" https://doi.org/10.1007/978-3-031-47705-8_4 " >DOI</a >
110+ (<a href =" https://rodrigo7491.github.io/files/papers/CHC_Model_Validation_with_Proof_Guarantees.pdf " >preprint</a >)
103111<br >
104112<i >Best Paper Award candidate</i >
105113</li >
@@ -109,27 +117,31 @@ C. Tirelli, <ins>R. Otoni</ins>, and L. Pozzi.
109117<b >Symbolic Model Checking for TLA+ Made Faster</b >.
11011829th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23).
111119<a href =" https://doi.org/10.1007/978-3-031-30823-9_7 " >DOI</a >
120+ (open access)
112121</li >
113122
114123<li >
115124<ins >R. Otoni</ins >, M. Blicha, P. Eugster, A. Hyvärinen, and N. Sharygina.
116125<b >Theory-Specific Proof Steps Witnessing Correctness of SMT Executions</b >.
11712658th ACM/IEEE Design Automation Conference (DAC'21).
118127<a href =" https://doi.org/10.1109/DAC18074.2021.9586272 " >DOI</a >
128+ (<a href =" https://rodrigo7491.github.io/files/papers/Theory-Specific_Proof_Steps_Witnessing_Correctness_of_SMT_Executions.pdf " >preprint</a >)
119129</li >
120130
121131<li >
122132M. Marescotti, <ins >R. Otoni</ins >, L. Alt, P. Eugster, A. Hyvärinen, and N. Sharygina.
123133<b >Accurate Smart Contract Verification Through Direct Modelling</b >.
1241349th International Symposium on Leveraging Applications of Formal Methods (ISoLA'20).
125135<a href =" https://doi.org/10.1007/978-3-030-61467-6_12 " >DOI</a >
136+ (<a href =" https://rodrigo7491.github.io/files/papers/Accurate_Smart_Contract_Verification_through_Direct_Modelling.pdf " >preprint</a >)
126137</li >
127138
128139<li >
129140<ins >R. Otoni</ins >, A. Cavalcanti, and A. Sampaio.
130141<b >Local Analysis of Determinism for CSP</b >.
13114220th Brazilian Symposium on Formal Methods (SBMF'17).
132143<a href =" https://doi.org/10.1007/978-3-319-70848-5_8 " >DOI</a >
144+ (<a href =" https://rodrigo7491.github.io/files/papers/Local_Analysis_of_Determinism_for_CSP.pdf " >preprint</a >)
133145</li >
134146
135147</ol >
@@ -151,13 +163,15 @@ A. Buccolini, M. Biasion, <ins>R. Otoni</ins>, G. Constantinides, and L. Pozzi.
151163<b >Automatisierte Garantierte Blockchain-Technologie Verifizierung</b >.
152164GI Ausgezeichnete Informatikdissertationen 2023 (Band 24), 2024.
153165<a href =" https://doi.org/10.18420/Diss2023-19 " >DOI</a >
166+ (open access)
154167</li >
155168
156169<li >
157170A. Buckley, P. Chuprikov, <ins >R. Otoni</ins >, R. Rand, R. Soulé, and P. Eugster.
158171<b >Towards an Algebraic Specification of Quantum Networks</b >.
1591721st Workshop on Quantum Networks and Distributed Quantum Computing (QuNet'23).
160173<a href =" https://doi.org/10.1145/3610251.3610557 " >DOI</a >
174+ (open access)
161175</li >
162176
163177</ol >
0 commit comments