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.


Publié dans:
Proceedings of the 6th ACM SIGPLAN Symposium on Scala - SCALA 2015, 35-40
Présenté à:
the 6th ACM SIGPLAN Symposium, Portland, OR, USA, 13 06 2015
Année
2015
Publisher:
New York, New York, USA, ACM Press
ISBN:
978-1-4503-3626-0
Mots-clefs:
Laboratoires:




 Notice créée le 2015-06-14, modifiée le 2018-03-17

Preprint:
Télécharger le documentPDF
Lien externe:
Télécharger le documentURL
Évaluer ce document:

Rate this document:
1
2
3
 
(Pas encore évalué)