Release 0.9.0

_layouts/home.html

@@ -55,7 +55,7 @@ <h2 class="title">
     our <a href="https://github.com/binsec/binsec/tree/master/doc">tutorials</a>. Further examples are bundled in our <a href="https://hub.docker.com/r/binsec/binsec">Docker image</a> and <a href="https://opam.ocaml.org/packages/binsec/">OPAM package</a>. 
     </p> 
 
-    <b>Current release is version 0.8 from 07/2023.</b>
+    <b>Current release is version 0.9 from 05/2024.</b>
 
     <p>We have frequent <b>job openings</b> for postdoc, PhD student and intern positions. Check up <a href="/#news">the news</a> for ongoing calls or <a href="/people/binsec.html">contact us</a> if you believe that you could be a good match.</p>
   </div>

_posts/2024-05-01-binsec-0.9.0.md

@@ -0,0 +1,25 @@
+---
+layout: post
+title:  "Release 0.9.0 of BINSEC is out"
+categories: releases binsec
+date: 2024-05-01
+github: https://github.com/binsec/binsec/releases/tag/0.9.0
+keywords: Incremental solving, IR-level sub-expression elimination
+---
+
+*Work less, work better*. Experiments tend to show it is a good way to increase the productivity.
+So, no shiny new feature today, but we shipped some improvements that may speed up the symbolic exploration!
+
+On the agenda:
+- take advantage of the incremental solving mode (`-sse-engine multi-checks`);
+- welcome the IR-level sub-expression elimination pass (`-sse-cse`).
+
+Overall, symbolic exploration spends most of its time in constraint solving.
+Besides, **BINSEC** used to open a new solver session for each issued query.
+But, let us now give a try to the incremental mode of SMT solvers. Within the `multi-checks` engine variant, **BINSEC** compares each new query with the previous one. If the latter is a parent of the former -- which often happens with the depth first search strategy -- **BINSEC** holds the session, both saving the setup time and thriving the prior solver knowledge.
+
+Less usual, but when the emulation speed becomes the exploration bottleneck (e.g. *France CyberSecurity Challenge* [licorne](https://github.com/binsec/binsec/blob/master/doc/sse/fcsc_licorne.md#bonus)), you can now activate the common sub-expression elimination pass to optimize the **BINSEC** intermediate representation and, hence, reduce the number of processed micro-instructions.
+
+Also, as a side announcement, we opened the [Discussions](https://github.com/binsec/binsec/discussions) section in the [GitHub](https://github.com/binsec/binsec) repository. Feel free to come and get help on how to use **BINSEC**.
+
+Have a nice day :-)