Citation
Uhler, R., & Dave, N. (2013, 13-19 July). Smten: automatic translation of high-level symbolic computations into SMT queries. Paper presented at the International Conference on Computer Aided Verification (CAV 2013), Saint Peterburg, Russia.
Abstract
Development of computer aided verification tools has greatly benefited from SMT technologies; instead of writing an ad-hoc reasoning
engine, designers translate their problem into SMT queries which solvers can efficiently solve. Translating a problem into effective SMT queries, however, is itself a tedious, error-prone, and non-trivial task. This paper introduces Smten, a tool for automatically translating high-level symbolic computations into SMT queries. We demonstrate the use of Smten in the development of an SMT-based string constraint solver.
