Home CU

  • VIS (Verification Interacting with Synthesis)
  • VIS is a system for formal verification, synthesis, and simulation of finite state systems. The formal verification part includes both BDD-based symbolic model checking for CTL and LTL, and SAT-based bounded model checking. 
  • CUDD (CU Decision Diagram Package)
  • CUDD is a package for the manipulation of Binary Decision Diagrams (BDDs), Algebraic Decision Diagrams (ADDs) and Zero-suppressed Binary Decision Diagrams (ZDDs). You can also download DDcal, a BDD calculator based on CUDD, PerlDD, an extension to Perl based on CUDD, and a collection of BDD variable orders
  • Wring
  • Wring is a program to translate Linear Time Logic (LTL) formulae into generalized Buechi automata. Wring is written in Perl. 
  • SatEEn is an SMT solver that deals with Quantifier-Free Linear Arithmetic Logic and Quantifier-Free Difference Logic. 
  • N_ABLE  (Action Based Learning for switching and automata theory)
  • N_ABLE consists of many interactive learning games for students interested in logic synthesis and verification. It is written in Java applets. 
    • Also check the Model Checking White Pages!

    • Which contains a list of people that are either involved in model checking, or of interest to people that do model checking. This page also has a list of research groups that do model checking, and a list of tools. 

    ECE Department | University of Colorado | Boulder Community | Webmaster

    Last Revision: