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

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.


Published in:
Proceedings of the 6th ACM SIGPLAN Symposium on Scala - SCALA 2015, 35-40
Presented at:
the 6th ACM SIGPLAN Symposium, Portland, OR, USA, 13 06 2015
Year:
2015
Publisher:
New York, New York, USA, ACM Press
ISBN:
978-1-4503-3626-0
Keywords:
Laboratories:




 Record created 2015-06-14, last modified 2018-09-13

Preprint:
Download fulltextPDF
External link:
Download fulltextURL
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)