Skip to content

Commit

Permalink
FM artifact: Cameleer only.
Browse files Browse the repository at this point in the history
  • Loading branch information
mariojppereira committed Jun 14, 2024
1 parent bf66b8e commit f7c1b19
Showing 1 changed file with 5 additions and 21 deletions.
26 changes: 5 additions & 21 deletions fm2024_artifact.html
Original file line number Diff line number Diff line change
Expand Up @@ -16,25 +16,20 @@ <h1>FM 2024 Artifact</h1>

<div id="content">
<p>This is a simple placeholder page for the companion artifact of the
submitted FM 2024 tutorial paper "The Theory and Practice of Deductive
Verification of OCaml Programs".</p>
conditionally accepted FM 2024 tutorial paper "Practical
Deductive Verification of OCaml Programs".</p>

<h2>Cameleer and CFML Repositories</h3>
<h2>Cameleer Repository</h3>

<p>Both projects present detailed instructions on to install the tools
and run them on examples.</p>
<p>Detailed instructions on to install the tools and run it on
examples:</p>

<ul>
<li><a href="https://github.com/ocaml-gospel/cameleer">Cameleer</a></li>
<li><a href="https://github.com/charguer/cfml/tree/queue">CFML</a></li>
(to build our case studies, we use specify a specific branch of the CFML
tool)
</ul>

<h2>Cases studies mentioned in the paper</h2>

<h3>Cameleer</h3>

<ul>
<li><a href="https://github.com/ocaml-gospel/cameleer/blob/master/examples/mergesort.ml">
Merge Routine</a></li>
Expand All @@ -52,17 +47,6 @@ <h3>Cameleer</h3>
Union Find</a></li>
</ul>

<h3>CFML</h3>

<ul>
<li><a href="https://github.com/charguer/cfml/tree/queue/examples/MList">
Linked-lists
</a></li>
<li><a href="https://github.com/charguer/cfml/tree/queue/examples/Queue">
OCaml Standard Library Queue
</a></li>
</ul>

<!-- <ul> -->
<!-- <li>The Virtual Box .ova file can be found -->
<!-- <a href="http://doi.org/10.5281/zenodo.4724119">here</a>.<p></p></li> -->
Expand Down

0 comments on commit f7c1b19

Please sign in to comment.