iimc/NEWS at master · mgudemann/iimc · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
IImc 2.0

New in this release:

 - Multi-threaded execution.
 - Bug fixes, code clean-up, and efficiency improvements.

IImc 2.0 has been built on:

 - Ubuntu 14.04 LTS and 14.10 with gcc and clang
 - Red Hat Fedora 21 with gcc and clang
 - Cygwin on Windows 7 and Vista, 32-bit, with gcc
 - Cygwin on Windows 8.1, 64-bit, with gcc
 - OS X 10.10.1 (yosemite) with clang

The versions of gcc range from 4.8.2 to 4.9.2.  The versions of clang
are 3.4 and 3.5.  At the time of this release, the distributed version
of clang on cygwin (3.4) does not support thread-local storage, and
therefore cannot be used to build IImc 2.0.

----------------------------------------------------------------------
IImc 1.4

New in this release:

 - Support for counterexample generation for safety properties
    - Can use AIGER format or native format
 - Reporting of lower bound on length of counterexample (if one exists)
    - So-called u-lines
 - k-liveness prototype
 - More timeout options for preprocessing tactics
 - Includes CUDD 2.5.1
 - Several bug fixes and efficiency improvements

IImc 1.4 has been built on:

 - Ubuntu 14.04 LTS and 14.10 with gcc and clang
 - Red Hat Fedora 21 with gcc and clang
 - Cygwin on Windows 7 and Vista, 32-bit, with gcc and clang
 - OS X 10.9.5 (mavericks) and 10.10.1 (yosemite) with clang

The versions of gcc range from 4.8.2 to 4.9.2.  The versions of clang
are 3.4 and 3.5.

----------------------------------------------------------------------
IImc 1.3.1

This is a bug-fixing release.  Notably, a problem with recent versions
of bison a bug in a test program exposed by gcc 4.8 have been fixed.

----------------------------------------------------------------------
IImc 1.3

New in this release:

 - Several improvements to IC3:
    - Lifting
    - CTGs (see FMCAD 2013 paper)
    - Localization reduction engine
 - Latest Minisat used for everything but IC3
 - Preprocessing:
    - TVsim (ternary simulation engine)
    - Phase abstraction
    - Slice
    - Decoding for backward encoded models
 - FCBMC (fair cycle BMC)
 - GSH (BDD-based cycle detection)
 - Several bugs fixes
 - Improved efficiency for large designs

IImc 1.3 has been built on:

 - Ubuntu 12.10, 13.04, and 13.10 with gcc
 - Ubuntu 12.10 with clang
 - Red Hat Enterprise 6.4 with gcc
 - Current Cygwin on Windows 7, both 32- and 64-bits, with gcc
 - OS X v10.7.5 and v10.8.5 with clang

The versions of gcc range from 4.4.7 to 4.8.2. Clang's version is 3.0.

----------------------------------------------------------------------
IImc 1.2

This is a bug-fix release.

----------------------------------------------------------------------
IImc 1.1

The major addition to IImc 1.1 is the new CTL model checking engine
from the CAV’12 paper: ”Incremental Inductive CTL Model Checking” by
Z. Hassan, A. R. Bradley, and F. Somenzi.

Additions in Release 1.1:

 - A new engine, IICTL, which is a new “IC3-like” model checking
   engine for CTL properties with fairness constraints
 - A new BMC engine for fair-cycle detection
 - Slightly improved performance for some of the model checking engines
 - A few bug fixes

IImc 1.1 has been compiled with g++ 4.4.6, 4.5.3, 4.6.3, 4.7.2, and
clang++ 3.0, and has been tested on Ubuntu 12.04 and 12.10, Red Hat
Enterprise 6.3, and Cygwin 1.7.

----------------------------------------------------------------------
IImc 1.0

This is the first release of IImc.  It features the following engines:

 - IC3 and IC3r
 - BDD-based forward and backward reachability analysis
 - BMC
 - FAIR

It is written in C++11 and has been compiled on Ubuntu and Cygwin.