Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries

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.

↓ Review online

Read more from SRI

  • The US Capitol Dome

    Quantum on Capitol Hill

    The SRI-managed Quantum Economic Development Consortium convened quantum innovators and members of Congress to explore the future of quantum technology.

  • Rays of light

    Building the photonic circuits of the future

    SRI’s work on DARPA’s HAPPI program seeks to measurably advance the capability of circuits that transmit information using light rather than electrons.

  • Turning AI into a problem-solving teammate

    To chart the future of human-machine teaming, SRI’s COLLEAGUE project is building an AI-based system designed to act as a true collaborative partner.