<?xml version="1.0"?>
<feed xmlns="http://www.w3.org/2005/Atom" xml:lang="en">
	<id>http://termination-portal.org/mediawiki/index.php?action=history&amp;feed=atom&amp;title=Tools%3AVeriFun</id>
	<title>Tools:VeriFun - Revision history</title>
	<link rel="self" type="application/atom+xml" href="http://termination-portal.org/mediawiki/index.php?action=history&amp;feed=atom&amp;title=Tools%3AVeriFun"/>
	<link rel="alternate" type="text/html" href="http://termination-portal.org/mediawiki/index.php?title=Tools:VeriFun&amp;action=history"/>
	<updated>2026-05-01T08:46:04Z</updated>
	<subtitle>Revision history for this page on the wiki</subtitle>
	<generator>MediaWiki 1.34.2</generator>
	<entry>
		<id>http://termination-portal.org/mediawiki/index.php?title=Tools:VeriFun&amp;diff=1759&amp;oldid=prev</id>
		<title>Christoph Walther at 00:09, 8 August 2017</title>
		<link rel="alternate" type="text/html" href="http://termination-portal.org/mediawiki/index.php?title=Tools:VeriFun&amp;diff=1759&amp;oldid=prev"/>
		<updated>2017-08-08T00:09:41Z</updated>

		<summary type="html">&lt;p&gt;&lt;/p&gt;
&lt;table class=&quot;diff diff-contentalign-left&quot; data-mw=&quot;interface&quot;&gt;
				&lt;col class=&quot;diff-marker&quot; /&gt;
				&lt;col class=&quot;diff-content&quot; /&gt;
				&lt;col class=&quot;diff-marker&quot; /&gt;
				&lt;col class=&quot;diff-content&quot; /&gt;
				&lt;tr class=&quot;diff-title&quot; lang=&quot;en&quot;&gt;
				&lt;td colspan=&quot;2&quot; style=&quot;background-color: #fff; color: #222; text-align: center;&quot;&gt;← Older revision&lt;/td&gt;
				&lt;td colspan=&quot;2&quot; style=&quot;background-color: #fff; color: #222; text-align: center;&quot;&gt;Revision as of 00:09, 8 August 2017&lt;/td&gt;
				&lt;/tr&gt;&lt;tr&gt;&lt;td colspan=&quot;2&quot; class=&quot;diff-lineno&quot; id=&quot;mw-diff-left-l13&quot; &gt;Line 13:&lt;/td&gt;
&lt;td colspan=&quot;2&quot; class=&quot;diff-lineno&quot;&gt;Line 13:&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;{{Tool&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;{{Tool&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;|shortname= VeriFun&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;|shortname= VeriFun&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt;−&lt;/td&gt;&lt;td style=&quot;color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;|longname= &lt;del class=&quot;diffchange diffchange-inline&quot;&gt;VeriFun - A Verifier &lt;/del&gt;for &lt;del class=&quot;diffchange diffchange-inline&quot;&gt;Functional Programs&lt;/del&gt;&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt;+&lt;/td&gt;&lt;td style=&quot;color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;|longname= &lt;ins class=&quot;diffchange diffchange-inline&quot;&gt;... a verifier &lt;/ins&gt;for &lt;ins class=&quot;diffchange diffchange-inline&quot;&gt;functional programs&lt;/ins&gt;&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;|homepage= http://verifun.de&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;|homepage= http://verifun.de&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;|country= Germany&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;|country= Germany&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;/table&gt;</summary>
		<author><name>Christoph Walther</name></author>
		
	</entry>
	<entry>
		<id>http://termination-portal.org/mediawiki/index.php?title=Tools:VeriFun&amp;diff=1758&amp;oldid=prev</id>
		<title>Christoph Walther: Created page with &quot; &lt;!--        Please fill in the data so that your tool can be added to some default        categories and a simple tool page can be created. You may extend        that tool pa...&quot;</title>
		<link rel="alternate" type="text/html" href="http://termination-portal.org/mediawiki/index.php?title=Tools:VeriFun&amp;diff=1758&amp;oldid=prev"/>
		<updated>2017-08-08T00:07:35Z</updated>

		<summary type="html">&lt;p&gt;Created page with &amp;quot; &amp;lt;!--        Please fill in the data so that your tool can be added to some default        categories and a simple tool page can be created. You may extend        that tool pa...&amp;quot;&lt;/p&gt;
&lt;p&gt;&lt;b&gt;New page&lt;/b&gt;&lt;/p&gt;&lt;div&gt;&lt;br /&gt;
&amp;lt;!--&lt;br /&gt;
       Please fill in the data so that your tool can be added to some default&lt;br /&gt;
       categories and a simple tool page can be created. You may extend&lt;br /&gt;
       that tool page yourself after the following code block.&lt;br /&gt;
&lt;br /&gt;
       Please use the &amp;quot;publication&amp;quot; field to add a reference to a publication&lt;br /&gt;
       introducing your tool. The &amp;quot;References&amp;quot; page can be used to enter a bibtex&lt;br /&gt;
       record for this publication.&lt;br /&gt;
       Example: |publication=[[Bibtex:Giesl04|Automated Termination Proofs with AProVE]]&lt;br /&gt;
--&amp;gt;&lt;br /&gt;
&lt;br /&gt;
{{Tool&lt;br /&gt;
|shortname= VeriFun&lt;br /&gt;
|longname= VeriFun - A Verifier for Functional Programs&lt;br /&gt;
|homepage= http://verifun.de&lt;br /&gt;
|country= Germany&lt;br /&gt;
|university= Technische Universität Darmstadt&lt;br /&gt;
|developers= Markus Aderhold, Visar Januzaj, Andreas Schlosser, Stephan Schweitzer, Simon Siegler, Christoph Walther, Nathan Wasser&lt;br /&gt;
|publication= Automated Termination Analysis for Programs with Second-Order Recursion; Automated Termination Analysis for Incompletely Defined Programs; On Proving the Termination of Algorithms by Machine (see http://verifun.de/Documents for details and more) &lt;br /&gt;
}}&lt;br /&gt;
&lt;br /&gt;
&amp;lt;!-- If you want to add some additional information to the tool page, you can do so after this comment. --&amp;gt;&lt;br /&gt;
VeriFun is a tool for verifying total correctness of functional programs. It uses a termination analysis based on the method of Argument-Bounded Functions which is automatically invoked upon the definition of a recursively defined procedure. The method aims to generate termination hypotheses which are sufficient for the procedure’s termination and are proved like lemmas. If the method fails to compute termination hypotheses, the user must provide an appropriate termination function. Afterwards induction axioms are computed from the terminating procedures’ recursion structure to be on stock for future use. See http://verifun.de/CaseStudies for a collection of examples from various domains.&lt;/div&gt;</summary>
		<author><name>Christoph Walther</name></author>
		
	</entry>
</feed>