metacsl and conc2seq

_data/plugins_categories.yml

@@ -19,5 +19,5 @@
 - name: Front-end for other languages
   key: front
 
-- name: For concurrent programs
+- name: For concurrent/multi-threaded programs
   key: concurrent

_fc-plugins/conc2seq.html

+---
+layout: plugin
+title: Conc2seq
+description: Verification of concurrent programs
+key: concurrent
+distrib_mode: proto
+---
+
+<dl class="defnitionList">
+  <dt class="subTitle">Overview</dt>
+  <dd><p>Conc2seq is dedicated to the verification of concurrent C
+      programs. More specifically, it proposes an instrumentation of the
+      original code that simulates all possible interleavings allowed by
+      the norm. The resulting instrumented code is then a sequential
+      programs that can be analyzed as such. Note however that the
+      transformation assumes that the original code is sequentially consistent,
+      which must be verified independently (e.g. by using the
+      <a href="mthread.html">Mthread plugin</a>).
+    </p>
+  </dd>
+  <dt class="subTitle">Use</dt>
+  <dd>
+    As the plugin is in an early stage of development, it is currently only
+    available upon request.
+  </dd>
+</dl>

_fc-plugins/metacsl.html

+---
+layout: plugin
+title: MetACSL
+description: Verification of meta-properties
+key: specifications
+distrib_mode: proto
+---
+
+<dl class="defnitionList">
+  <dt class="subTitle">Overview</dt>
+  <dd><p>MetACSL is a plug-in dedicated
+      to specifying and verifying
+      <i>Meta Properties</i>, that is properties that are supposed
+      to be checked at many points of the code base under analysis,
+      so that writing the corresponding ACSL annotations manually
+      would be extremely tedious and error-prone. A simple example
+      of such a property would be a confidentiality property indicating
+      that no access to a particular memory block should occur unless
+      some clearance condition holds. Specifying that in pure ACSL
+      would require writing an assertion for each reading access in the
+      code, while MetACSL only needs a single meta-property.
+    </p>
+    <p>In summary, MetACSL defines a global ACSL extension for describing
+      meta properties, that are composed of three things:
+      <ul>
+        <li>a target, the set of functions where the meta-property should hold.
+        </li>
+        <li>a context, the kind of program points that are concerned by the
+          meta-property. Two important contexts are <tt>\writing</tt> and
+          <tt>\reading</tt> accesses.</li>
+        <li>the property itself. It is an ACSL predicate, possibly enriched
+          with meta-variables depending on the context. For instance,
+          a <tt>\writing</tt> context gives rise to a <tt>\written</tt>
+          meta-variable denoting the location being written to.
+        </li>
+      </ul>
+      The plug-in proceeds by generating all ACSL annotations corresponding to
+      each meta-property. It is then possible to use one of the main analysis
+      plug-ins of the platform (e.g. <a href="wp.html">WP</a>,
+      <a href="e-acsl.html">E-ACSL</a>, or <a href="eva.html">Eva</a>) to
+      verify these annotations.
+    </p>
+  </dd>
+  <dt class="subTitle">Use</dt>
+  <dd>
+    As the plugin is in an early stage of development, it is currently only
+    available upon request.
+  </dd>
+</dl>