Lectures

• Lecture 1 (PDF)
• Lecture 2 (PDF)
• seahorn-tutorial

Tools

• SeaHorn on GitHub
• Vagrant box with all the pre-requisites to run and build SeaHorn: seahorn-dev32.box.

  mkdir seahorn ; cd seahorn
  vagrant box add seahorn seahorn-dev32.box
  vagrant init seahorn
  vagrant up
  vagrant ssh

• Standalone VirtualBox VM. Only use if vagrant is not available. seahorn-dev32-vbox.ova (username: vagrant, password: vagrant)
• SeaHorn pre-build build environment. Unpack into /Vagrant directory: seahorn-build.tar.bz2

  vagrant ssh
  cd /Vagrant
  tar xvjf seahorn-build.tar.bz2 

• Spacer on Bitbucket

Suggested Reading

1. A. Gurfinkel, T. Kahsai, and J. A. Navas, Algorithmic Logic-Based Verification. (PDF)
2. A. Gurfinkel, T. Kahsai, A. Komuravelli, and J. A. Navas, The SeaHorn Verification Framework. (PDF)
3. N. Bjørner, A. Gurfinkel, K. McMillan, and A. Rybalchenko, Horn Clause Solvers for Program Verification. (PDF)
4. A. Gurfnkel, IC3, PDR, and Friends. (PDF)
5. A. Komuravelli, A. Gurfinkel, and S. Chaki, SMT-based Model Checking for Recursive Programs. (arXiv)
6. N. Bjørner and A. Gurfinkel, Property Directed Polyhedral Abstraction. (PDF)
7. A. Komuravelli, N. Bjørner, A. Gurfinkel, K. McMillan, Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. (PDF)

Other References

1. LLVM Language Reference Manual