This repository has been archived by the owner on Dec 1, 2018. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
93 lines (72 loc) · 3.31 KB
/
index.html
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
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
<head>
<meta charset="utf-8"/>
<title>Artifact evaluation</title>
<meta name="author" content="Soonho Kong"/>
<meta name="date" content="15 Apr 2018"/>
<link type="text/css" rel="stylesheet" href="css/tufte.css"/>
</head>
<body>
<p>Artifact evaluation of the following paper.</p>
<pre><code>Delta-Decision Procedures for Exists-Forall Problems over the Reals
Soonho Kong, Armando Solar-Lezama, and Sicun Gao
In CAV (International Conference on Computer Aided Verification) 2018
</code></pre>
<h2 id="virtualmachine">Virtual Machine</h2>
<ul>
<li> Image File: <a href="http://www.cs.cmu.edu/~soonhok/CAV18_Paper248_AE.ova">http://www.cs.cmu.edu/~soonhok/CAV18_Paper248_AE.ova</a></li>
<li> SHA256 of Image: <code>b6c3d4c476ac67e2e495fc2ac741cbf2d34b74443d560d28efe8f14b452716de</code></li>
<li> OS: ubuntu-16.04.4-desktop-amd64</li>
<li> Account (ID/Password): cav / ae</li>
<li> Host Platform: 2017 Macbook Pro with 2.9 GHz Intel Core i7
(QuadCore) and 16 GB RAM running MacOS 10.13.4</li>
</ul>
<h2 id="coverage">Coverage</h2>
<ul>
<li> Section 5.1 Nonlinear Global Optimization
<ul>
<li>Table 1.</li>
</ul></li>
<li> Section 5.2 Synthesizing Lyapunov Function for Dynamical System
<ul>
<li>Normalized Pendulum</li>
<li>Damped Mathieu System</li>
</ul></li>
</ul>
<h2 id="instructions">Instructions</h2>
<p>Log in the provided VM (ID: <code>cav</code>, PASSWORD: <code>ae</code>). Open a terminal
and execute the following instructions.</p>
<ul>
<li><p> Table 1 in Section 5.1 (Expected Running Time <= 5min)</p>
<pre><code>./dreal4/bazel-bin/dreal/api/cav18_benchmark
./dreal4/bazel-bin/dreal/api/cav18_benchmark --local-optimization
</code></pre>
<p><a href="https://github.com/dreal/dreal4/blob/c37dfdbb64c2bb15c8f9d7250d20e98c53b948e5/dreal/api/test/cav18_benchmark.py">[Source Code]</a></p></li>
<li><p> Normalized Pendulum in Section 5.2 (Expected Running Time <= 1min)</p>
<pre><code>./dreal4/bazel-bin/dreal/examples/synthesize_lyapunov_normalized_pendulum
</code></pre>
<p><a href="https://github.com/dreal/dreal4/blob/master/dreal/examples/synthesize_lyapunov_normalized_pendulum.cc">[Source Code]</a></p></li>
<li><p> Damped Mathieu System in Section 5.2 (Expected Running Time <= 1min)</p>
<pre><code>./dreal4/bazel-bin/dreal/examples/synthesize_lyapunov_damped_mathieu
</code></pre>
<p><a href="https://github.com/dreal/dreal4/blob/master/dreal/examples/synthesize_lyapunov_damped_mathieu.cc">[Source Code]</a></p></li>
</ul>
<h2 id="quality">Quality</h2>
<ul>
<li> Source code of the implementation, dReal4, is available at
<a href="https://github.com/dreal/dreal4/tree/cav18">https://github.com/dreal/dreal4/tree/cav18</a>.</li>
<li> Its
<a href="https://github.com/dreal/dreal4/blob/master/README.md">README.md</a>
file provides build and install instructions.</li>
<li> Source code is documented using Doxygen. Documentation webpage is
at
<a href="https://dreal.github.io/dreal4">https://dreal.github.io/dreal4</a>.</li>
<li> We provide a comprehensive set of unittests, which can be executed by running
“<code>bazel test //...</code>”.</li>
<li> We provide packages for macOS (via homebrew) and Debian/Ubuntu
Linux. The instructions are in the
<a href="https://github.com/dreal/dreal4/blob/master/README.md">README.md</a>.</li>
</ul>
</body>
</html>