Zot is an open and easily extendable bounded model/satisfiability checker. It was born as a satisfiability checker, as its original language is the TRIO metric temporal logic. Zot now supports operational, descriptive, or hybrid models. Its plug-in based architecture permits both mono- and bi-infinite discrete temporal domains (i.e. infinite both towards the past and the future), and also supports a dense-time variant of the MTL logic.
Note: there is a new Zot page here.
Download sources (release 20110606)