-
Notifications
You must be signed in to change notification settings - Fork 1
/
INSTALL
125 lines (94 loc) · 4.17 KB
/
INSTALL
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
116
117
118
119
120
121
122
123
124
125
Jahob preliminary version of 20 August 2012.
This version corrects several bugs and adds several capabilities contributed by
Alexander Malkis. The main of them are:
- the switch "-tryHard" for a further aggressive splitting of verification
conditions.
- handling cardinalities of comprehensions of finite sets before calling
a decision procedure for BAPA.
Required:
make, version >= 3.81
ocaml, version >= 3.12.1
gcc, version >= 4.6.2
Recommended:
mona, version >= v1.4-13
spass, version >= 3.7
cvc3, version >= 2.2
z3, version >= 3.2
Compilation:
vim lib/cudd/Makefile
# adapt XCFLAGS for your machine
cd src
make clean && make depend && make all
------------------------------------------------------------
Jahob preliminary version of 8 April 2007.
This distribution is meant for students of the EPFL class
Software Analysis and Verification 2007, taught by Viktor Kuncak.
It contains simpler make files for formDecider, namely
Makefile.formDecider and Makefile.formDecider.opt.
On the technical side it contains many important improvements of the
underlying analyses and decision procedures which have not all been
documented yet and should not be relied on or reverse engineered.
------------------------------------------------------------
Jahob preliminary version of 23 July 2006.
This version adds the following key improvements implemented by
Charles Bouillaguet that joins the Jahob team:
* TPTP interfaces to first-order theorem provers
* SPASS interface (works with SPASS 3.7)
(try downloading executables with as eprover and SPASS)
* Coq interface
* complete hiding of objects
It also incorporates numerous improvements for Bohne, developed
by Thomas Wies, and a new version of verification condition generator
written by Viktor Kuncak, invoked by -sastvc.
There are other features and changes that are currently not
documented, but we decided to release the updated sources
anyway. Documentation should appear in a few months at
most. We have more extensive set of libraries and a
regression suite that you can run
------------------------------------------------------------
Jahob preliminary version of 1 February 2006.
This is a preliminary distribution.
Please let us know if you are planing to use it.
More installation friendly distribution might come soon.
(c) Viktor Kuncak ([email protected])
Thomas Wies ([email protected])
Karen Zee ([email protected])
Huu Hai Nguyen ([email protected])
Peter Schmitt ([email protected])
The wrote written by us is released under GPL and MIT
licence (make your pick), see files COPYING.* . We are using
Caddie, which you can use under their own licences.
MIT licence should allow any reasonable use of this system, but let us
know if you have a problem.
Instalation instructions (verified under Debian distribution with kernel
Linux 2.6.8-1-686-smp #1 SMP Thu Nov 25 04:55:00 UTC 2004 i686 GNU/Linux).
Required:
make
ocaml distribution (tested with ocamlc version 3.09.1)
Instalation instructions:
Untar the distribution
Type make to create bytecode compiled versions
This will produce executable bin/jahob directory
Type
cd src; make -f Makefile.opt depend; make -f Makefile.opt ../bin/jahob.opt
This will produce native code compiled executables.
We run executables by doing cd into the appropriate example subdirectory
and then running something like:
../../../bin/jahob JavaFile1.java JavaFile2.java -method JavaFile1.methodName -nobackground -usedp mona isa cvcl
Executables will place their temporary files in
the ../tmp/ directory relative
to where their position.
Jahob can use the following external programs
(with the corresponding executable names):
MONA - used for analyzing linked data structures
http://www.brics.dk/mona/
Isabelle cvs snapshot from 24 February 2005 - useful fallback
http://www4.informatik.tu-muenchen.de/~isabelle/
CVC Light (or other SMT-LIB compatible prover; we only tested it with CVCL)
http://chicory.stanford.edu/CVCL/
Simplify, not essential (Simplify)
only minimal support
Omega Calculator (oc)
http://www.cs.umd.edu/projects/omega/
LASH executable, not essential (presburger)
- an alternative for Omega, usually worse