Model Checking for the Practical Verificationist:
A User's Perspective on SAL

• ABSTRACT:
  
  SRI's Symbolic Analysis Laboratory (SAL) is a high-level language-interface to a collection of state-of-the-art model checking tools. SAL contains novel and powerful features, many of which are not available in other model checkers. In this experience report, I highlight some of the features I have particularly found useful, drawing examples from published verifications using SAL. In particular, I discuss the use of higher-order functions in model checking, infinite-state bounded model checking, compositional specification and verification, and finally, mechanical theorem prover and model checker interplay. The purpose of this report is to expose these features to working verificationists and to demonstrate how to exploit them effectively.

• BIBTEX:
  

  @inproceedings{pike-afm,
    author    = {Lee Pike},
    title     = {Model checking for the practical verificationist: a user's perspective on {SAL}},
    booktitle = {Proceedings of the Automated Formal Methods Workshop (AFM07)},
    year      = {2007},
    publisher = {ACM Press},
    note      = {Available at \url{https://leepike.github.io/pub_pages/afm07.html}}}
  

• PAPER DOWNLOAD: pdf 

• SLIDES DOWNLOAD:
  • Talk slides: pdf
  • SAL file supporting the paper and talk: pikeAFM.sal

• ADDENDUM:
  In Section 3.2 of the paper, I did not make explicit that the straight-forward definition of of chanSet in the paper requires that the two transition guards, H and I, must be mutually exclusive.