pass over README

README.md

@@ -5,15 +5,17 @@
 
 <img align="right" width="150" src="logo.png"/>
 
-Raven (Resource Algebra Verification ENgine) is an SMT-based deductive verifier for concurrent separation logic. Raven supports features like invariants, custom user-defined resource algebras ("monoids"), and a powerful higher-order module system that enables code and proof re-use. Raven also has smart heuristics that automate many low-level details, and an inlined style of development that interleaves code and proof. This streamlines the process of co-developing a program alongside its proof of correctness.
+Raven is an intermediate verification language and SMT-based deductive verifier based on concurrent separation logic. It is intended as an intermediate layer for building program verification tools that target concurrent programs. Raven can also be used as a standalone educational tool.
 
-Raven provides a highly-automated, user-friendly front-end that draws heavily from projects like [Dafny](https://github.com/dafny-lang/dafny) and [Viper](https://www.pm.inf.ethz.ch/research/viper.html). Raven has a sizeable, and growing [collection](test/concurrent) of verified implementations of fine-grained concurrent data structures commonly found in the literature and as well as real systems.
+Raven's language design draws inspiration from projects like [Boogie](https://www.microsoft.com/en-us/research/project/boogie-an-intermediate-verification-language/) and [Viper](https://www.pm.inf.ethz.ch/research/viper.html) but treats concurrency as a first-class citizen. 
+Raven has a sizeable, and growing [collection](test/concurrent) of verified implementations of fine-grained concurrent data structures commonly found in the literature as well as real systems.
 
-These implementations are then translated to first-order logic and passed to the [Z3](https://github.com/Z3Prover/z3) SMT-solver to determine whether the user-provided input verifies successfully.
+Raven supports features like *shareable* invariants, user-definable resource algebras ("monoids"), and a higher-order module system that enables code and proof reuse. Its inlined style of development, interleaving code and proof, streamlines the process of co-developing a program alongside its proof of correctness. The Raven verifier then translates Raven programs to verification conditions expressed in first-order logic, which are then automatically dispatched using the SMT solver [Z3](https://github.com/Z3Prover/z3).
 
-Raven also ships with a [library](lib/library/resource_algebra.rav) of standard resource algebra implementations, as well as higher-order resource algebra constructors that embody commonly occuring patterns in proofs of concurrent data structures. This helps the user get started with proofs quickly.
+Raven ships with a [library](lib/library/resource_algebra.rav) of standard resource algebra definitions, as well as higher-order resource algebra constructors that embody commonly occurring patterns in proofs of concurrent data structures. This helps the user get started with proofs quickly.
+
+Raven's underlying meta-theory is based on the [Iris](https://iris-project.org/) separation logic framework. We simplify the Iris logic by carefully restricting its features (like higher-order quantification, impredicativity, and step-indexing). At the same time, we add complementary features like the higher-order module system to regain expressivity. The resulting logic is sufficiently expressive to verify complex concurrent algorithms, yet, amenable to robust SMT-based automation. The mechanization of Raven's program logic as an instance of the Iris framework is part of ongoing work.
 
-Raven's underlying separation logic is based on the [Iris](https://iris-project.org/) separation logic framework. We vastly simplify the Iris logic by carefully restricting its most higher-order features (like impredicativity and step-indexing). This results in a sufficiently expressive logic that is amenable to robust SMT-based automation. Developing a formal proof of Raven's compatibility with Iris is part of ongoing-work.
 
 ## Installation
 Raven can be installed by running the following sequence of commmands. It requires [opam](https://opam.ocaml.org/).
@@ -27,16 +29,16 @@ $ dune build; dune install; dune runtest
 ```
 
 ## Examples
-Several examples can be found in the [test](test) folder. The [ci](test/ci) folder contains many small example that can be used to learn Raven syntax for specific features. Complete verified implementations of concurrent data structures can be found in the [concurrent](test/concurrent) folder. Here are a few notable ones to get started, in roughly increasing order of complexity:
+Several examples of Raven programs can be found in the [test](test) folder. The [ci](test/ci) folder contains many small examples that can be used to learn Raven's syntax for specific features. Complete verified implementations of concurrent data structures can be found in the [concurrent](test/concurrent) folder. Here are a few notable ones to get started, in roughly increasing order of complexity:
 1. [spin_lock](test/concurrent/lock/spin-lock.rav)
 1. [monotonic_counter](test/concurrent/counter/counter_monotonic.rav)
 1. [treiber_stack](test/concurrent/treiber_stack/treiber_stack_atomics.rav)
 1. [atomic_resource_counter](test/comparison/arc_atomics.rav)
-1. [bplustree](test/concurrent/templates/bplustree.rav)
 1. [give-up template](test/concurrent/templates/give-up.rav)
+1. [bplustree](test/concurrent/templates/bplustree.rav)
 
 ## Usage
-Raven can be executed on a file `test/concurrent/treiber_stack/treiber_stack_atomics.rav` as follows:
+The Raven verifier can be executed on a file `test/concurrent/treiber_stack/treiber_stack_atomics.rav` as follows:
 ```
 $ raven test/concurrent/treiber_stack/treiber_stack_atomics.rav
 Raven version 1.0
@@ -45,14 +47,14 @@ Verification successful.
 Here is a failing example:
 ```
 $ raven test/ci/back-end/fail/fpu_fail.rav
-Raven version 1.
+Raven version 1.0
 [Error] File "test/ci/back-end/fail/fpu_fail.rav", line 7, columns 2-14:
 7 |   fpu(x.f, 4);
       ^^^^^^^^^^^^
 Verification Error: This update may not be frame-preserving.
 ```
 
-### Raven Manual
+### Raven Verifier Manual
 ```
 RAVEN(1)                         Raven Manual                         RAVEN(1)
 
@@ -67,6 +69,10 @@ ARGUMENTS
            Input file.
 
 OPTIONS
+       --base-dir=VAL
+           Base directory for resolving include directives. Default: current
+           working directory.
+           
        --color=WHEN (absent=auto)
            Colorize the output. WHEN must be one of auto, always or never.