Sound reasoning about integral data types with a reusable SMT solver interface

We extend the Leon verification system for Scala with support for bitvector reasoning, thus addressing one of its fundamental soundness limitation with respect to the treatment of integers primitives. We leverage significant progresses recently achieved in SMT solving by developing a solver-independent interface to easily configure the back-end of Leon. Our interface is based on the emerging SMT-LIB standard for SMT solvers, and we release a Scala library offering full support for the latest version of the standard. We use the standard BigInt Scala library to represent mathematical integers, whereas we correctly model Int as 32-bit integers. We ensure safety of arithmetic by checking for division by zero and correctly modeling division and modulo. We conclude with a performance comparison between the sound representation of Ints and the cleaner abstract representation using mathematical integers, and discuss the trade-off involved.

• Type: Journal
• Year: 2015
• Where: PLDI
• Authors: Régis Blanc, Viktor Kuncak
• Keywords: PLDI 2015, Programming Languages