Enhancing the Satisfiability Modulo Theories Experience (Smten)
Development of tools for computer aided verification has greatly benefited from Satisfiability Module Theories (SMT) technologies; instead of writing an ad-hoc reasoning engine, tool developers translate their problem into SMT queries which solvers can efficiently solve. In practice, translating a problem into effective SMT queries is a tedious, error-prone, and non-trivial task. Smten is a unified language for general-purpose functional programming and SMT query orchestration whose goal is to greatly simplify the development of practical SMT-based tools for computer aided verification.
We are developing an open-source implementation of the Smten language as a plugin to the Glasgow Haskell Compiler which supports the full syntax of the Haskell functional programming language. Our implementation currently supports SMT solvers Yices1, Yices2, Z3, and STP. The source code and additional documentation for Smten is available on github here.
- Hampi: String Constraint Solver
As an illustration of the conciseness and flexibility of design in Smten, we reimplemented the string constraint solver HAMPI. The resulting SHAMPI tool is of comparable performance at 20x fewer lines of code, and it has the ability to completely change the low-level theories and SMT solvers used in solving the string constraints. See below for results of this work as presented at CAV2013. The source code for SHAMPI is available on github here.
- Simulation Verification of Bluespec SystemVerilog Designs
Bluespec StystemVerilog is a hardware description language centered around the notion of guarded atomic actions (GAAs) to improve hardware design modularity and reuse. GAAs have a natural correspondence to term rewrite systems, which have seen significant use in formal analysis. Despite this, there has been relatively limited progress in leveraging Bluespec's semantic model for formal analysis. We are implementing a variation of a recently proposed GAA-based simulation technique that mechanically extracts an architectural view from a microarchitectural design given a predicate representing that view. This can be used to quickly extract a specification-level representation of a design which can be much more easily checked, either by hand or mechanically. We are in the process of scaling up the performance to provide a fast abstraction of the CHERI processor.
Smten in CAV 2013
Richard Uhler, Nirav Dave. Smten: Automatic Translation of High-level Symbolic Computations into SMT Queries. In: Proceedings of the 25th International Conference on Computer Aided Verification (CAV 2013).