2013 | OriginalPaper | Chapter
Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries
Authors : Richard Uhler, Nirav Dave
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.