postscript,
pdf
This is a fairly complete description of the SAL language for specifying transition systems. Note that the IMPLEMENTS operator is not implemented (!) and that the assertion language is not defined as part of SAL but by the tools that interpret the assertions. The model checkers use LTL (Linear Temporal Logic) as their assertion language (they also accept CTL syntax on the common fragment); please see the basic tutorial (below) and the FAQ for more details.
SAL and XML - SAL is intended to be language and platform independent; toward this end we defined the abstract syntax for the SAL language in XML. The SAL DTD describes valid abstract syntax.
postscript,
pdf
This is a very elementary tutorial; it introduces the LTL assertion language, and use of the symbolic and bounded model checkers and some auxiliary tools
This is a more substantial example from the field of fault-tolerant algorithms; it uses both the symbolic and bounded model checkers
This is another fairly substantial example, this time from the field of cryptographic protocols; it uses both the symbolic and bounded model checkers