author | blanchet |
Fri, 30 May 2014 12:27:51 +0200 | |
changeset 57120 | f8112c4b9cb8 |
parent 52098 | 6c38df1d294a |
permissions | -rw-r--r-- |
52098
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
1 |
<HR><!------------------------------------------------------------------------> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
2 |
<H2>Nitrox 2013</H2> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
3 |
Jasmin C. Blanchette<sup>1</sup>, Emina Torlak<sup>2</sup><BR> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
4 |
<sup>1</sup>Technische Universität München, Germany <BR> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
5 |
<sup>2</sup>University of California, Berkeley, USA <BR> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
6 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
7 |
<H3>Architecture</H3> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
8 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
9 |
Nitrox is the first-order version of Nitpick [<A HREF="#References">BN10</A>], |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
10 |
an open source counterexample generator for Isabelle/HOL |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
11 |
[<A HREF="#References">NPW13</A>]. It builds on Kodkod |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
12 |
[<A HREF="#References">TJ07</A>], a highly optimized first-order relational |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
13 |
model finder based on SAT. The name Nitrox is a portmanteau of <b><i>Nit</i></b>pick |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
14 |
and Pa<b><i>r</i></b>ad<b><i>ox</i></b> (clever, eh?). |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
15 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
16 |
<H3>Strategies</H3> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
17 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
18 |
<p> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
19 |
Nitrox employs Kodkod to find a finite model of the negated conjecture. It |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
20 |
performs a few transformations on the input, such as pushing quantifiers inside, |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
21 |
but 99% of the solving logic is in Kodkod and the underlying SAT solver. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
22 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
23 |
<p> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
24 |
The translation from HOL to Kodkod's first-order relational logic (FORL) is |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
25 |
parameterized by the cardinalities of the atomic types occurring in it. Nitrox |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
26 |
enumerates the possible cardinalities for the universe. If a formula has a |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
27 |
finite counterexample, the tool eventually finds it, unless it runs out of |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
28 |
resources. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
29 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
30 |
<p> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
31 |
Nitpick is optimized to work with higher-order logic (HOL) and its definitional |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
32 |
principles (e.g., (co)inductive predicates, (co)inductive datatypes, |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
33 |
(co)recursive functions). When invoked on untyped first-order problem, few of |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
34 |
its optimizations come into play, and the problem handed to Kodkod is |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
35 |
essentially a first-order relational logic (FORL) rendering of the TPTP FOF |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
36 |
problem. There are two main exceptions: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
37 |
<ul> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
38 |
<li> Nested quantifiers are moved as far inside the formula as possible before |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
39 |
Kodkod gets a chance to look at them [<A HREF="#References">BN10</A>]. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
40 |
<li> Definitions invoked with fixed arguments are specialized. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
41 |
</ul> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
42 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
43 |
<H3>Implementation</H3> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
44 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
45 |
<p> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
46 |
Nitrox, like most of Isabelle/HOL, is written in Standard ML. Unlike Isabelle |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
47 |
itself, which adheres to the LCF small-kernel discipline, Nitrox does not |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
48 |
certify its results and must be trusted. Kodkod is written in Java. MiniSat 1.14 |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
49 |
is used as the SAT solver. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
50 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
51 |
<H3>Expected Competition Performance</H3> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
52 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
53 |
Since Nitpick was designed for HOL, it doesn't have any type inference à |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
54 |
la Paradox. It also doesn't use the SAT solver incrementally, which penalizes it |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
55 |
a bit (but not as much as the missing type inference). Kodkod itself is known to |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
56 |
perform less well on FOF than Paradox, because it is designed and optimized for |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
57 |
a somewhat different logic, FORL. On the other hand, Kodkod's symmetry breaking |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
58 |
might be better calibrated than Paradox's. Hence, we expect Nitrox to end up in |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
59 |
second or third place in the FNT category. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
60 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
61 |
<H3>References</H3> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
62 |
<DL> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
63 |
<DT> BN10 |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
64 |
<DD> Blanchette J. C., Nipkow T. (2010), |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
65 |
<STRONG>Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder</STRONG>, |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
66 |
ITP 2010, <EM>LNCS</EM> 6172, pp. 131–146, Springer. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
67 |
<DT> NPW13 |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
68 |
<DD> Nipkow T., Paulson L. C., Wenzel M. (2013), |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
69 |
<STRONG>Isabelle/HOL: A Proof Assistant for Higher-Order Logic</STRONG>, |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
70 |
<A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf">http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf</a>. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
71 |
<DT> TJ07 |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
72 |
<DD> Torlak E., Jackson D. (2007), |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
73 |
<STRONG>Kodkod: A Relational Model Finder</STRONG>, TACAS 2007, |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
74 |
<EM>LNCS</EM> 4424, pp. 632–647, Springer. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
75 |
</DL> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
76 |
<P> |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
77 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
78 |
<HR><!------------------------------------------------------------------------> |