Skip to content

Commit 67ec425

Browse files
committed
Remove outdated information
1 parent 423630e commit 67ec425

File tree

1 file changed

+0
-9
lines changed

1 file changed

+0
-9
lines changed

trunk/source/WebsiteStatic/config/tool_pages/buechi_automizer.html

Lines changed: 0 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -15,15 +15,6 @@ <h1>Büchi Automizer</h1>
1515
<h2>Web Interface</h2>
1616
<p> <span style="font-variant:small-caps">Ultimate</span> Automizer is available via a <a href="?ui=int&tool=buechi_automizer">web interface</a> in which you can analyse termination of C programs. This version has some limitations. We use a theorem prover that does not support non-linear arithmetic and therefore the built-in tool <a href="?ui=int&tool=lasso_ranker">LassoRanker</a> can only provide linear ranking functions.</p>
1717

18-
<h2>Commandline Version</h2>
19-
<p>Ultimate Büchi Automizer and the built-in tool <a href="?ui=int&tool=lasso_ranker">LassoRanker</a> are in heavy development. A recent version is available on request, please contact <a href="http://swt.informatik.uni-freiburg.de/staff/heizmann">Matthias Heizmann</a>.</p>
20-
21-
<h2>Commandline Version (CAV 2014 Submission)</h2>
22-
<p>The <a href="http://ultimate.informatik.uni-freiburg.de/downloads/BuchiAutomizer/cav2014/UltimateCommandline.zip">commandline version</a> that was used for the evaluation in our CAV 2014 submission is available. This version runs on x86-64 linux machines and has some limitations. In our evaluation we showed the potential ouf our method to prove termination of a general program while using only simple termination arguments for lasso-shaped traces. Therefore, we restricted the built-in tool <a href="http://ultimate.informatik.uni-freiburg.de/LassoRanker">LassoRanker</a> to linear ranking functions.</p>
23-
24-
<h2>Commandline Version (SV-COMP 2014)</h2>
25-
<p>The <a href="http://ultimate.informatik.uni-freiburg.de/downloads/BuchiAutomizer/svcomp2014/UltimateCommandline.zip">commandline version</a> that was our competition candidate for the demonstration category on termination at the <a href="http://sv-comp.sosy-lab.org/2014/">SV-COMP 2014</a>. This version runs on x86-64 Linux machines and requires that the <a href="http://z3.codeplex.com/"> theorem prover Z3</a> is installed. In this version, the built-in tool <a href="http://ultimate.informatik.uni-freiburg.de/LassoRanker">LassoRanker</a> is limited to linear ranking functions and multiphase ranking functions.</p>
26-
2718
<h2>Developers</h2>
2819
<p>Ultimate Buchi Automizer is maintained by <a href="http://swt.informatik.uni-freiburg.de/staff/heizmann">Matthias Heizmann</a>. The built-in tool <a href="?ui=int&tool=lasso_ranker">LassoRanker</a> is maintained by <a href="http://swt.informatik.uni-freiburg.de/staff/leike">Jan Leike</a> and <a href="http://swt.informatik.uni-freiburg.de/staff/heizmann">Matthias Heizmann</a>.
2920
Since <span style="font-variant:small-caps">Ultimate</span> Büchi Automizer is a toolchain of the <a href="http://ultimate.informatik.uni-freiburg.de"><span style="font-variant:small-caps">Ultimate</span> software analysis framework</a>, <a href="#developers">many people</a> contributed code and ideas. We want to mention especially, Jürgen Christ, Daniel Dietsch, Jochen Hoenicke,

0 commit comments

Comments
 (0)