Rodrigo Otoni is a postdoctoral researcher at USI Lugano, Switzerland, working on approaches for automated reasoning in the contexts of verification, synthesis, and certification. He is experienced with model checking, SMT and CHC solving, TLA+ specifications, and process algebras, as well as smart contracts and other blockchain technologies.