« Tech talk video: Program Inconsistency Detection Using Weakest Preconditions | Main | Tech talk: Program Inconsistency Detection using Weakest Preconditions »
Tuesday
Jan182011

Merging SMT solvers and programming languages

Galois is in the business of building trustworthy software. Such software will have well-defined behavior, and that behavior is assured in some way, whether via model checking, testing, or formal verification. SMT solvers -- extensions to SAT solvers with support for variables of non-boolean type -- offer powerful automation for solving a variety of assurance problems in software. We use them, for example, in Cryptol, to prove the equivalence (or otherwise) of algorithm implementations.


For a while now, Galois has been interested in connecting automated solvers to our programming language of choice, Haskell, to make it possible to prove automatically some properties of our functions (rather than just testing, e.g. with QuickCheck). We've pushed two efforts out this week, as previews of what we're thinking in this space:





Both are embedded DSLs for representing propositions to an SMT solver via Haskell functions and values. They take different approaches (a compiler from Haskell to the SMT-LIB format, versus an interpreter for the Yices SMT solver). SBV is the more mature package, while yices-painless emphasizes a type-preserving translation from a minimal core language. SBV was built by Levent Erkok, yices-painless by Don Stewart. Documentation for the design of yices-painless is available, as is documentation on SBV.


Both are ready for experimentation and feedback, and we welcome your comments.

Reader Comments (2)

To my knowledge SMT solvers are unable to reason (co-)inductively and so can't construct proofs over lists/trees or any user-defined recursive data-type. This means that you can only solve imperative model-checking style problems over primitive/enumerated data-types. That being said I think this is a great piece of work and will be very helpful for this style of problem, which is very prevalent in real-life programs.Note: My hypothesis is that this is a fundamental incompatibility with the DPLL(T) algorithm, in that the theory T would have to do perform the inductive step in its propositional truth check, which is much too complex (not to mention incomplete) for a DPLL(T) theory, and would need to have DPLL assignment steps in between for a complex proof. I'm not sure since I don't work within SMT solving but I'd love some clarification on this.
January 19, 2011 | Unregistered CommenterWill
Hi,Thanks for this work! It turns out that by hooking up SMT with the language's type system, it is quite possible to get some, highly automated inductive reasoning about lists, trees etc.paper: http://pho.ucsd.edu/rjhala/papers/type-based_data_structure_verification.pdfonline demo: http://pho.ucsd.edu/liquid/demo/index2.phpIn the course of pushing the above work, we have been looking around for ways to hook into SMT solvers from within Haskell, so thanks for SBV and yices-painless!Ranjit.
January 19, 2011 | Unregistered CommenterRanjit Jhala

PostPost a New Comment

Enter your information below to add a new comment.

My response is on my own website »
Author Email (optional):
Author URL (optional):
Post:
 
Some HTML allowed: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <code> <em> <i> <strike> <strong>