The purpose of the workshop is to share ideas on the two close topics : static and dynamic code analysis and compilation. By encouraging discussions and co-operations across different, yet related fields, the workshop strives for bridging the gap between the two communities.
Topics include :
Static and dynamic analysis techniques (abstract interpretation, SMT-solving, bounded model checking, typing, proof-carrying code. . . ) to be integrated into compilers.
Studies on the design of statics analysers : frontends, impact of intermediate representations (CFG,
SSA) on precision and efficiency of static analysers.
Talks should be accessible to the combined audience of the workshop, and emphasize areas where
compilation and static analysis techniques interact.
We feel that there are already many venues that accept papers on such topics, and that the “refereed papers and printed proceedings” format stiffles discussion, which is what a workshop should be
about. As a consequence, we have opted for the following format :
One keynote speech. It will be delivered by Sandrine Blazy. Sandrine is one of the main architects of the CompCert compiler, which compiles C to a variety of CPU targets. So far, not so extraordinary; but what is extraordinary is that CompCert has been proved to be semantically correct within the Coq proof assistant. That is, the exists a mathematical proof that, if the compiler produces some output, then this output truly implements the source code; and this proof has been mechanically checked. This is a rather amazing achievement, which mixes consideration of strong semantic soundness (common in the formal methods and static analysis community) with pragmatic compilation requirements.
A series of presentations, which we encourage to be less formal than in a conference.
We strongly encourage submissions of presentations that would be attractive for the combined
audience of the workshop (experts in compilation, program analysis and program proofs). However
the proposals might not fit within the usual conference format. For instance, we encourage reports
of experience with building analysis systems or compilers, which might not contain new results,
but may help the audience a great deal by conveying practical insights.
List of accepted Talks
Compiler-driven Optimization of the Worst-Case Execution Time Florian Brandner and Alain Darte.
Dependencies between Analyses and Transformations in the
Middle-End of a Compiler Francois Irigoin, Fabie Coelho and
Beatrice Creusillet.
Analyze to verify compilation; Verify compilation to
analyze Xavier Rival.
Static Loops Analysis in Concurrent Programs Lakhdar-Chaouch Lies, Jeannet Bertrand and Girault Alain.
Bringing IR Interpretation to Compilers for Analysis
Purpose Nicolas Benoit and Stéphane Louise.
Submission and important dates
Submission was handled
by EasyChair
(http://www.easychair.org/conferences/?conf=acca2011). Authors
had to submit a an abstract of their talk, up to 1
page.
