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

  • surgeons around a surgical robot

    The SRI research behind today’s surgical robotics

    Intuitive’s da Vinci 5 system represents a major leap in robotic-assisted medicine. It all started at SRI, which continues to advance teleoperation technologies.

  • a collage of digital graphs

    A banner year for quantum

    SRI-managed QED-C’s annual report on quantum trends captures an industry accelerating rapidly from technical promise toward major global impact.

  • ICE Cube containing SRI’s aerogel experiment, photographed prior to launch. Source: Aerospace Applications North America

    An SRI carbon capture experiment launches into space

    By synthesizing carbon-absorbing aerogels in microgravity, SRI research will give us a rare glimpse into how these materials could be radically improved.