Juliano Iyoda is interested in formal methods applied to hardware and software design, automated reasoning (in particular, the HOL theorem proving system) and testing.