Automated SMT-based Verification for Reasoning about Approximations

October 16, 2015
Zvonimir Rakamaric | University of Utah

Approximate computing is an emerging area for trading off the accuracy of an application for improved performance, lower energy costs, and tolerance to unreliable hardware. However, care has to be taken to ensure that the approximations do not cause significant divergence from the reference implementation. Previous research has proposed various metrics to guarantee several relaxed notions of safety for the design and verification of such approximate applications. However, current approximation verification approaches often lack in either precision or automation. On one end of the spectrum, type-based approaches lack precision, while on the other, proofs in interactive theorem provers require significant manual effort.

In this work, we apply automated differential program verification (as implemented in SymDiff) for reasoning about approximations. We show that mutual summaries naturally express many relaxed specifications for approximations, and SMT-based checking and invariant inference can substantially automate the verification of such specifications. We demonstrate that the framework significantly improves automation compared to previous work. In addition, our approach can verify an important class of relaxed specifications related to program termination. Our results indicate the feasibility of applying automated verification to the domain of approximate computing in a cost-effective manner.

Speaker Details

Zvonimir Rakamaric is an assistant professor in the School of Computing at the University of Utah. Prior to this, he was a postdoctoral fellow at Carnegie Mellon University in Silicon Valley, where he worked closely with researchers from the Robust Software Engineering Group at NASA Ames Research Center to improve the coverage of testing of NASA’s flight critical systems. Zvonimir received his bachelor’s degree in Computer Science from the University of Zagreb, Croatia; he obtained his M.Sc. and Ph.D. from the Department of Computer Science at the University of British Columbia, Canada.

Zvonimir’s research mission is to improve the reliability and resilience of complex software systems by empowering developers with practical tools and techniques for analysis of their artifacts. He is a recipient of the Microsoft Research Software Engineering Innovation Foundation (SEIF) Award 2012, Microsoft Research Graduate Fellowship 2008-2010, Silver Medal in the ACM Student Research Competition at the 32nd International Conference on Software Engineering (ICSE) 2010, and the Outstanding Student Paper Award at the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2007.