Commit c1cf2b38 authored by Sven Keidel's avatar Sven Keidel

add explanation of OOPSLA paper to the README

parent c517e5b2
Pipeline #15839 passed with stages
in 36 minutes and 33 seconds
# Sturdy ![build-status](https://travis-ci.org/svenkeidel/sturdy.svg?branch=master)
<img align="left" alt="Sturdy Logo" src="/logo.svg" width="30%" height="15%">
<img align="left" alt="Sturdy Logo" src="/logo.svg" width="25%">
Sturdy is a library to create sound static analyses in Haskell.
Static analyses are tools that produce information about computer programs without actually running the program.
Examples of static analyses are type checkers, bug finders (e.g. Java FindBugs), analyses for security (e.g. taint analyses), and analyses that are used for compiler optimizations.
<img align="right" alt="Sturdy Overview" src="/overview.png">
This project focuses on _sound_ static analyses.
A static analysis is sound if the results of the analysis reflect the actual runtime behavior of the program and users can rely on the results.
For example, if a static analysis used for compiler optimizations were unsound, the optimization might change the semantics of the program, which leads to unexpected behavior at runtime.
To this end, Sturdy follows the theory of _Compositional Soundness Proofs of Abstract Interpreters_ to simplify soundness proofs of static analyses.
To this end, Sturdy follows the theory of _Compositional Soundness Proofs of Abstract Interpreters_ and _Sound and Reusable Components for Abstract Interpretation_ to simplify soundness proofs of static analyses.
<img align="right" alt="Sturdy Overview" src="/overview.png">
In short, Sturdy factorizes the concrete interpreter and abstract interpreter (the static analysis) into a _generic interpreter_.
Sturdy factorizes the concrete interpreter and abstract interpreter (the static analysis) into a _generic interpreter_.
This generic interpreter is parameterized by interfaces that contain primitive operations that describe the semantics of the language, such as `try`, `catch` and `finally` for exceptions.
The concrete and abstract interpreter then instantiate the generic interpreter by implementing these interfaces.
This reorganization not only decouples different concerns in the implementation of the static analysis, but also in the its soundness proof.
More details can be found in the [paper](https://dl.acm.org/citation.cfm?id=3236767).
This reorganization not only decouples different concerns in the implementation of the static analysis, but also simplifies its soundness proof.
More details can be found in our [ICFP paper](https://dl.acm.org/citation.cfm?id=3236767).
Sturdy allows to construct static analyses modularly from reusable analysis components.
Each analysis component encapsulates a single analysis concern and can be proven sound independently from the analysis where it is used.
Furthermore, the theory of analysis components guarantees that a static analysis is sound, if all its analysis components are sound.
This means that analysis developers do not have to worry about soundness as long as they reuse sound analysis components.
More details can be found in our [OOPSLA paper](https://svenkeidel.de/papers/analysis-components.pdf).
## Getting Started
......
......@@ -17,10 +17,13 @@
id="svg4327"
sodipodi:docname="logo.svg"
inkscape:version="0.92.4 (5da689c313, 2019-01-14)"
style="fill-rule:evenodd;stroke-width:28.22200012;stroke-linejoin:round"><metadata
style="fill-rule:evenodd;stroke-width:28.22200012;stroke-linejoin:round"
inkscape:export-filename="/home/sven/documents/sturdy/logo.png"
inkscape:export-xdpi="96"
inkscape:export-ydpi="96"><metadata
id="metadata4331"><rdf:RDF><cc:Work
rdf:about=""><dc:format>image/svg+xml</dc:format><dc:type
rdf:resource="http://purl.org/dc/dcmitype/StillImage" /><dc:title></dc:title></cc:Work></rdf:RDF></metadata><sodipodi:namedview
rdf:resource="http://purl.org/dc/dcmitype/StillImage" /><dc:title /></cc:Work></rdf:RDF></metadata><sodipodi:namedview
pagecolor="#ffffff"
bordercolor="#666666"
borderopacity="1"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment