Dr. Ran Ettinger is a Senior Engineer at NVIDIA, developing tools and methodologies for the formal verification of software, combining bounded model checking with deductive verification for proving correctness of sequential and concurrent programs. In teaching, as an adjunct lecturer at Ben-Gurion University of the Negev and in the Israel Academic College of Ramat Gan he is employing formal method techniques both in elective programming courses (at BGU using Dafny and SPARK) and more recently in required courses (at IAC using Dafny) on the foundational subjects of Logic and Set Theory as well as Formal Languages and Automata Theory. A passionate proof engineer and an experienced programmer with a history of research on static analysis of programs and on tools for software maintenance (IBM Research, Sun Microsystems Laboratories), Rani holds a Doctor of Philosophy degree from the University of Oxford (2008) and a Bachelor of Science degree in Mathematics and Computer Science from BGU (2000).