Rodrigo Otoni is a postdoctoral fellow at the Università della Svizzera italiana, Switzerland. He is experienced with model checking, SMT and CHC solving, TLA+ specifications, and process algebras, as well as smart contracts and other blockchain technologies.