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