A Verified Model Checker for Conjunctive Positive Logic

    TTM: A Tableau-based Theorem Prover for Temporal Logic PLTL

    BCN Prototype: An implementation of Constructive Negation

    CS Prototype: An equality constraint solver