ANNOUNCE
changeset 33881 d8958955ecb5
parent 33873 e9120a7b2779
child 33914 d17f447fec02
equal deleted inserted replaced
33880:6cc01403f78a 33881:d8958955ecb5
    14 with equality, linear and nonlinear (natural/integer/real) arithmetic,
    14 with equality, linear and nonlinear (natural/integer/real) arithmetic,
    15 and fixed-size bitvectors.
    15 and fixed-size bitvectors.
    16 
    16 
    17 * HOL-Boogie: an interactive prover back-end for Boogie and VCC.
    17 * HOL-Boogie: an interactive prover back-end for Boogie and VCC.
    18 
    18 
    19 * HOL: Counterexample generator tool Nitpick based on the Kodkod
    19 * HOL: counterexample generator tool Nitpick based on the Kodkod
    20 relational model finder.
    20 relational model finder.
    21 
    21 
    22 * HOL: predicate compiler turning inductive into (executable)
    22 * HOL: predicate compiler turning inductive into (executable)
    23 equational specifications.
    23 equational specifications.
    24 
    24