SMT solving with SBV

This repository contains all the resources for my talk for the Brisbane Functional Programming Group on 10 July 2018.

Dependencies

You'll need a few things on your system:

• GSL version 2, to simulate the pendulum system with hmatrix-gsl.

• Cairo, to generate plots with Chart-cairo

• The Z3 SMT solver (or optionally some other SMT solver that SBV supports, but the code will look for Z3 as written)

Slide dependencies

There's plenty of other stuff required to generate the slides:

• Texlive (pdflatex)
• pdftocairo
• pandoc

Source code

The code is all in Pendulum.hs. The main function runs some simulations, emits plots and generates C code. You should be able to produce an executable that does this with cabal build or stack build.

Running the proofs

Load up Pendulum.hs into GHCI, then invoke either proveStability or proveNanSafety. Be advised that this may take a long time!

Building the slides

You can use the provided Makefile or follow the steps below.

Generate trajectory plots

The plots of the pendulum trajectories were generated by running the provided executable after building the code. I did it with

stack exec pendulum

Generate the pendulum diagram

The pendulum diagram was generated from the included pendulum-diagram.tex file with the command

pdflatex pendulum-diagram.tex

and converted to an SVG with

pdftocairo -svg pendulum-diagram.pdf pendulum-diagram.svg

Build the slides into HTML

The slides on the Github Pages site were then generated by running the following command:

pandoc --webtex https://latex.codecogs.com/svg.latex? -s -t slidy -o smt-solving.html smt-solving.md

Note that you need to generate the pendulum trajectory plots before rendering the slides to HTML.