000208956 001__ 208956
000208956 005__ 20180913063148.0
000208956 020__ $$a978-1-4503-3626-0
000208956 0247_ $$2doi$$a10.1145/2774975.2774980
000208956 037__ $$aCONF
000208956 245__ $$aSound reasoning about integral data types with a reusable SMT solver interface
000208956 269__ $$a2015
000208956 260__ $$aNew York, New York, USA$$bACM Press$$c2015
000208956 336__ $$aConference Papers
000208956 520__ $$aWe 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.
000208956 6531_ $$averification
000208956 6531_ $$asoftware reliability
000208956 6531_ $$asmt solvers
000208956 700__ $$aBlanc, Régis
000208956 700__ $$0240031$$aKuncak, Viktor$$g177241
000208956 7112_ $$athe 6th ACM SIGPLAN Symposium$$cPortland, OR, USA$$d13 06 2015
000208956 773__ $$q35-40$$tProceedings of the 6th ACM SIGPLAN Symposium on Scala - SCALA 2015
000208956 8564_ $$uhttp://dl.acm.org/citation.cfm?doid=2774975.2774980$$zURL
000208956 8564_ $$s448534$$uhttps://infoscience.epfl.ch/record/208956/files/main.pdf$$yPreprint$$zPreprint
000208956 909C0 $$0252019$$pLARA$$xU11739
000208956 909CO $$ooai:infoscience.tind.io:208956$$pconf$$pIC
000208956 917Z8 $$x175339
000208956 937__ $$aEPFL-CONF-208956
000208956 973__ $$aEPFL$$rREVIEWED$$sPUBLISHED
000208956 980__ $$aCONF