Abstract: |
We present a framework for the development of certified static
analyses using the Coq proof assistant. Several challenges will be
addressed in this talk: How do we scale up the development of
certified analyses to real languages (like bytecode Java)? Rather than
formalise a single analysis, can we propose a family of analyses,
parameterised by a precision/efficiency factor? We will propose some
solutions to these questions through the example of an
inter-procedural abstract interpreter for the Java bytecode language.
|