Software

• SKOLEM: Solves the Skolem Problem for simple integer linear recurrence sequences.
  

• POROUS: An invariant builder and reachability checker for affine programs.
  See also this paper.

• SLAP: A static livelock analyser for CSP processes (now bundled within FDR).
  See also this paper, this paper, and this paper.

• APEX: A verification tool for probabilistic programs.
  See also this paper, this paper, this paper, and this paper.

• MAGIC: A model checker for sequential and concurrent C programs.
  See also this paper, this paper, this paper, this paper, this paper, this paper, and this paper.

• UCLID: A verification tool for infinite-state systems.
  (Implemented by S. K. Lahiri and S. A. Seshia.)
  See also this paper, this paper, and this paper.