Blanc, RĂ©gis
Kuncak, Viktor
Sound reasoning about integral data types with a reusable SMT solver interface
Proceedings of the 6th ACM SIGPLAN Symposium on Scala - SCALA 2015
Proceedings of the 6th ACM SIGPLAN Symposium on Scala - SCALA 2015
Proceedings of the 6th ACM SIGPLAN Symposium on Scala - SCALA 2015
Proceedings of the 6th ACM SIGPLAN Symposium on Scala - SCALA 2015
verification
software reliability
smt solvers
2015
2015
We extend the Leon verification system for Scala with support for bit-vector 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.
ACM Press
978-1-4503-3626-0
Proceedings of the 6th ACM SIGPLAN Symposium on Scala - SCALA 2015
Conference Papers
10.1145/2774975.2774980