termite-analyser.github.io/index.html at master · termite-analyser/termite-analyser.github.io · 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

<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
    <title>Termite - Termination analyser</title>
    <meta name="Author" content="Laure Gonnord">
    <meta name="description" content="termite">
    <meta name="keywords" content="pldi,termite,rank">
    <link rel="stylesheet" href="termite.css" type="text/css">
  </head>

  <body>

    <header>
      <h1>Termite - Termination analyser</h1>
      <img src="logo_VERIMAG_vectorise.svg" alt="VERIMAG logo"
	         class="logo"/>

      <img src="logo_lip.png" alt="LIP logo"
	         class="logo"/>

    </header>


    <h3>Research paper</h3>

    <ul>
      <li>Termite's algorithm was presented in  "Synthesis of ranking
        functions using extremal counterexamples", <a href="http://conf.researchr.org/home/pldi2015">PLDI'15</a></li>
      <li>The author version of the paper
        is <a href="https://hal.archives-ouvertes.fr/hal-01144622">here</a>.</li>
      <li><a href="termite.bib">Bibtex file</a></li>
      <li>Coming soon : our video presentation for PLDI.</li>
    </ul>


    <h3>Source code/ Experimental results</h3>
    <ul>
      <img src="termite_tool.png" alt="Termite tool"
	         class="toolchain"/>
      <li>The invariant generator we use is <a href="http://pagai.forge.imag.fr">Pagai</a></li>
      <li>Termite is based on many open source components available <a href="https://github.com/termite-analyser">on github</a>:
        <ul>
          <li>An overlay for the ocaml z3 bindings that enables type-safe creation of SMT formulas: <a href="https://github.com/termite-analyser/z3overlay">z3overlay</a></li>
          <li>LLVM2SMT provides an SMT-encoding of the llvm-ir
            graph: <a href="https://github.com/termite-analyser/llvm2smt">llvm2smt</a></li>
          <li><a href="https://github.com/termite-analyser/termite">termite</a> itself.
        </ul>
        <br/>

      <li>Instalation instructions using opam are available <a href="https://github.com/termite-analyser/opam-termite#opam-repository-for-termite-packages">here</a>.</li>
      <li> <a href="results/results.html">Comparaison with other
          termination tools</a> on Ubuntu 64bits </li>
    </ul>


    <h3>Authors</h3>
    <ul>
      <li>Laure Gonnord</li>
      <li>David Monniaux</li>
      <li>Gabriel Radanne</li>
    </ul>

    <h3>Credits</h3>
    <ul>
      <li> Marc Vincenti, for the scripts </li>
      <li> Julien Henry, for the css file </li>
    </ul>

  </body>
</html>