Commit 1e15ece0 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

ROBDD webpage

parent e3c5b882c216
......@@ -3608,3 +3608,17 @@ abstract =
in the traces of the first operand. Both of these assumptions are
shown, by means of counterexamples, to be necessary for the theorem to
hold.
[ROBDD]
title = Algorithms for Reduced Ordered Binary Decision Diagrams
author = Julius Michaelis <http://liftm.de/>, Maximilian Haslbeck <https://home.in.tum.de/~haslbecm/>, Peter Lammich <https://www21.in.tum.de/~lammich/>, Lars Hupel <https://www21.in.tum.de/~hupel/>
date = 2016-04-27
topic = Computer Science/Algorithms, Computer Science/Data Structures
abstract =
We present a verified and executable implementation of ROBDDs in
Isabelle/HOL. Our implementation relates pointer-based computation in
the Heap monad to operations on an abstract definition of boolean
functions. Internally, we implemented the if-then-else combinator in a
recursive fashion, following the Shannon decomposition of the argument
functions. The implementation mixes and adapts known techniques and is
built with efficiency in mind.
<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="../front.css">
<script src="../jquery.min.js"></script>
<script src="../script.js"></script>
<link rel="icon" href="../images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<table width="100%">
<tbody>
<tr>
<td width="20%" align="center" valign="top">
<!-- navigation -->
<!--#include file="nav.html"-->
</td>
<td width="80%" valign="top">
<!-- content -->
<div align="center">
<p>&nbsp;</p>
<h1><font class="first">A</font>lgorithms
for
<font class="first">R</font>educed
<font class="first">O</font>rdered
<font class="first">B</font>inary
<font class="first">D</font>ecision
<font class="first">D</font>iagrams
</h1>
<p></p>
<table width="80%" class="data">
<tbody>
<tr><td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">Algorithms for Reduced Ordered Binary Decision Diagrams</td></tr>
<tr><td class="datahead">Author:</td>
<td class="data"><a href="http://liftm.de/">Julius Michaelis</a>, <a href="https://home.in.tum.de/~haslbecm/">Maximilian Haslbeck</a>, <a href="https://www21.in.tum.de/~lammich/">Peter Lammich</a> and <a href="https://www21.in.tum.de/~hupel/">Lars Hupel</a></td></tr>
<tr><td class="datahead">Submission date:</td>
<td class="data">2016-04-27</td></tr>
<tr><td class="datahead" valign="top">Abstract:</td>
<td class="abstract">
We present a verified and executable implementation of ROBDDs in
Isabelle/HOL. Our implementation relates pointer-based computation in
the Heap monad to operations on an abstract definition of boolean
functions. Internally, we implemented the if-then-else combinator in a
recursive fashion, following the Shannon decomposition of the argument
functions. The implementation mixes and adapts known techniques and is
built with efficiency in mind.
</td></tr>
<tr><td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{ROBDD-AFP,
author = {Julius Michaelis and Maximilian Haslbeck and Peter Lammich and Lars Hupel},
title = {Algorithms for Reduced Ordered Binary Decision Diagrams},
journal = {Archive of Formal Proofs},
month = apr,
year = 2016,
note = {\url{http://isa-afp.org/entries/ROBDD.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Automatic_Refinement.shtml">Automatic_Refinement</a>, <a href="Separation_Logic_Imperative_HOL.shtml">Separation_Logic_Imperative_HOL</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
<!---INCLUDE- file="devel-warning.shtml"-->
</tbody>
</table>
<p></p>
<!--#set var="name" value="ROBDD" -->
<!--#set var="binfo" value="../browser_info/current/AFP/${name}" -->
<!--#set var="doc" value="${binfo}/document.pdf" -->
<!--#set var="outline" value="${binfo}/outline.pdf" -->
<!--#set var="browse" value="${binfo}/index.html" -->
<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->
<table class="links">
<tbody>
<tr>
<td class="links">
<a href="<!--#echo var="outline" -->">Proof outline</a><br>
<a href="<!--#echo var="doc" -->">Proof document</a>
</td>
<!-- link to README.hmtl if no document exists -->
</tr>
<tr>
<td class="links">
<a href="<!--#echo var="browse" -->">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="<!--#echo var="tar" -->">Download this entry</a>
</td>
</tr>
<tr><td class="links">Older releases:
None </td></tr>
</tbody>
</table>
<!-- entry data end -->
</td> </tr> </table>
</body>
</html>
......@@ -49,6 +49,16 @@ A <a href="devel.shtml">development version</a> of the archive is available as w
<td class="head">2016</td>
</tr>
<tr><td class="entry">
2016-04-27:
<a href="entries/ROBDD.shtml">Algorithms for Reduced Ordered Binary Decision Diagrams</a>
<br>Author:
<a href="http://liftm.de/">Julius Michaelis</a>,
<a href="https://home.in.tum.de/~haslbecm/">Maximilian Haslbeck</a>,
<a href="https://www21.in.tum.de/~lammich/">Peter Lammich</a> and
<a href="https://www21.in.tum.de/~hupel/">Lars Hupel</a>
</td></tr>
<tr><td class="entry">
2016-04-26:
<a href="entries/Noninterference_Sequential_Composition.shtml">Conservation of CSP Noninterference Security under Sequential Composition</a>
......
......@@ -85,6 +85,7 @@
<a href="entries/Hermite.shtml">Hermite</a> &nbsp;
<a href="entries/Imperative_Insertion_Sort.shtml">Imperative_Insertion_Sort</a> &nbsp;
<a href="entries/Formal_SSA.shtml">Formal_SSA</a> &nbsp;
<a href="entries/ROBDD.shtml">ROBDD</a> &nbsp;
<strong>Distributed:</strong>&nbsp;<a href="entries/DiskPaxos.shtml">DiskPaxos</a> &nbsp;
<a href="entries/GenClock.shtml">GenClock</a> &nbsp;
......@@ -129,6 +130,7 @@
<a href="entries/IEEE_Floating_Point.shtml">IEEE_Floating_Point</a> &nbsp;
<a href="entries/Native_Word.shtml">Native_Word</a> &nbsp;
<a href="entries/XML.shtml">XML</a> &nbsp;
<a href="entries/ROBDD.shtml">ROBDD</a> &nbsp;
</div>
<h3>Functional Programming</h3>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment