SpaceSearch: A library for building and verifying solver-aided tools

Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, Zachary Tatlock
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 17 October 2019

ICFP 2017: Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming
Oxford, UK
Pages 25:1-25:28
September 2017
Topic(s): tools verification
Note(s): Rosette solver, Coq theorem prover
Papers: torlak:pldi:2014

Coq embedding of Rosette’s solver aided language inspired by smten.

Factors proof into two parts with SpaceSearch ADT as the interface between the two.

  • Coq proof (interactive) - can use induction, coinduction, higher order, etc.
  • Rosette proof (automatic) - limited to first order.

Demonstrated by

  • verifying RockSalt against STOKE
  • verifying Bagpipe

Found bugs in both.

Rosette solver