Verification Techniques for Low-Level Programs

Date and time: 
Thursday, February 21, 2019 - 13:00
260 Deschutes
Samuel Pollard
University of Oregon
  • Boyana Norris (chair)
  • Hank Childs
  • Zena Ariola

We explore the application of highly expressive logical and automated reasoning techniques to the analysis of computer programs. Some techniques generate programs which are correct by construction while others analyze and verify properties of existing programs. We provide an introduction to the field of formal methods and describe different tools and the strength of the properties they can guarantee. Additionally, we look at the verification of floating point arithmetic and fine-grained parallelism, such as Single-Instruction Multiple Data (SIMD) parallelism. Throughout, we focus on verification techniques applied to programs written in binary, bytecode, intermediate representations, and assembly languages.