Tidy

src/tutorial.adoc

@@ -6,7 +6,7 @@
 :sectanchors:
 :toc: left
 :stylesheet: style.css
-Christopher Pulte; Benjamin C. Pierce; with contributions from Elizabeth Austell
+By Christopher Pulte and Benjamin C. Pierce, with contributions from Elizabeth Austell
 
 [abstract]
 --
@@ -15,23 +15,20 @@ CN is a type system for verifying C code, focusing especially on low-level syste
 This tutorial introduces CN along a series of examples, starting with basic usage of CN on simple arithmetic functions and slowly moving towards more elaborate separation logic specifications of data structures. 
 
 CN was first described in https://dl.acm.org/doi/10.1145/3571194[CN: Verifying Systems C Code with Separation-Logic Refinement Types] by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami.
-// 
+//
 To accurately handle the complex semantics of C, CN builds on the https://github.com/rems-project/cerberus/[Cerberus semantics for C].
-// 
+//
 Some of the examples in this tutorial are adapted from Arthur Charguéraud’s excellent
 https://softwarefoundations.cis.upenn.edu[Separation Logic
-Foundations] textbook.
+Foundations] textbook, and one of the case studies is based on an
+extended exercise due to Bryan Parno.
 
 This tutorial is a work in progress -- your suggestions are greatly appreciated!
---
-
-{nbsp} +
-{nbsp} +
-
-
 
 **Acknowledgment of Support and Disclaimer.**
-This material is based upon work supported by the Air Force Research Laboratory (AFRL) and Defense Advanced Research Projects Agencies (DARPA) under Contract No. FA8750-24-C-B044, a European Research Council (ERC) Advanced Grant “ELVER” under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 789108), and additional funding from Google.  Any opinion, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Air Force Research Laboratory (AFRL).
+This material is based upon work supported by the Air Force Research Laboratory (AFRL) and Defense Advanced Research Projects Agencies (DARPA) under Contract No. FA8750-24-C-B044, a European Research Council (ERC) Advanced Grant “ELVER” under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 789108), and additional funding from Google.  The opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the Air Force Research Laboratory (AFRL).
+
+--
 
 == Installing CN