Added intro, ref, author.

README.md

 # Polymalys
 
+Polymalys: Polyhedra-based Memory Analysis.
+
+* Version XX for Otawa XX
+
+----
+## Author
+
+Clement Ballabriga <Clement.Ballabriga@nospamuniv-lille.fr>
+
+License: GPL 2.1 or higher.
+
+Please remove "nospam" from the email address.
+
+----
+
+## Introduction
+
+Polymalys is a tool for static analysis of *binary* code. It discovers
+linear relations between data locations (i.e. memory locations as well
+as registers) of the code. The analysis relies on abstract
+interpretation using a polyhedra-based abstract domain. The current
+implementation exploits the discovered linear relations to compute upper
+bounds to loop iterations. For more information on the underlying
+theory, refer to [1].
+
 ## Requirements
 
 * Parma Polyhedra Library (PPL): http://bugseng.com/products/ppl/
@@ -87,17 +112,21 @@ cd tests
 Read `tests/poly.cpp`
 
 
-## Known limitations (future works):
+## Future works
 
- * No modular inter-procedural analysis
- * No support for integer wrap/overflow
- * Loops with equality (instead of inequality) in loop condition will have pessimistic bounds
- * We assume that each memory access has 32bits-size, and is 32bits-aligned
+ * Use discovered linear relations for other static analyses:
+   out-of-stack accesses detection, dead-code detection, ...
+ * Inter-procedural analysis
+ * Support for integer wrap/overflow
+ * Loops conditions with equality tests (instead of inequality)
+   currently have pessimistic bounds
+ * We currently assume that each memory access has 32bits-size, and is 32bits-aligned
  * Lots of speed optimization needs to be done
 
+----
+## References
 
-## Questions:
-
-mail: Clement.Ballabriga@univ-lille1.fr
-
-
+[1] Ballabriga, C., Forget, J., Gonnord, L., Lipari, G. and Ruiz, J.,
+2019, January. Static Analysis Of Binary Code With Memory Indirections
+Using Polyhedra. In International Conference on Verification, Model
+Checking, and Abstract Interpretation (pp. 114-135).