Software

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

• SLAP: A static livelock analyser for CSP processes.
  See also 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.