-
Notifications
You must be signed in to change notification settings - Fork 2
Home
Canal is a static analysis tool designed to analyze behaviour of application programs written in C. It is a research project based on the theoretical framework of abstract interpretation, with focus on the scalability to large programs and proper handling of real-world source code.
The development is graciously supported by Red Hat and Masaryk University.
Download now: canal-2.zip.
See Canal 2 Release Notes.
The upcoming release is Canal 3. You can track its progress in the Third release milestone.
Canal has a small team of contributors and lots of interesting experiments waiting to be done. If you are a developer, you can join us to advance practical static analysis of application programs. If you are a student, check the bachelor and master thesis topics.
- Karel Klíč (project management): xklic at fi.muni.cz
- Tomáš Brukner (integer abstract domains): tomas.brukner at gmail.com
- Matej Šuta (string abstract domains): suta.matej at gmail.com
- Jan Dupal (reduced product): dupal.j at gmail.com
Project status is discussed on weekly meetings, held Tuesdays at 5pm in room G219, 1st floor of building B in Gotex, Šumavská 15, Brno, Czech Republic. The meetings are public and you are welcomed to come. Various topics related to Canal and its applications can be discussed.
- Tue 2013-02-05
- Tue 2013-01-29
- Tue 2013-01-15
- Tue 2013-01-08
- Tue 2012-11-27
- Tue 2012-11-20
- Tue 2012-11-13
- Tue 2012-11-06
- Tue 2012-10-30
- Tue 2012-10-23
- Tue 2012-10-16
- Tue 2012-10-09
- Tue 2012-10-02
- Tue 2012-09-25
- Tue 2012-09-18
- Continuous Integration of the git repository
- Profiling of Canal: measure space and time complexity of the analyzer
- Integer Domains Implementation State
- Abstract interpretation overviews:
- RWTH Aachen Course: Static Program Analysis
- MIT Course 16.399: Abstract Interpretation
- International Winter School on Semantics and Applications Course: Abstract interpretation and static analysis
- Abstract Interpretation References
- Events related to abstract interpretation
- Foundations:
- Brian Albert Davey and Hilary Ann Priestley. Introduction to Lattices and Order. 2nd ed. Cambridge University Press, 2002.
- David A. Schmidt. Denotational Semantics: A Methodology for Language Development. 2007.
- Roland Backhouse, Roy Crole, and Jeremy Gibbons, eds. [[Algebraic and Coalgebraic Methods in the Mathematics of Program Construction|http://books.google.cz/books/about/Introduction_to_Lattices_and_Order.html?id=vVVTxeuiyvQC]]. Springer-Verlag, 2002.
- LLVM:
- Chris Lattner and Vikram Adve. [[LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation|http://llvm.org/pubs/2004-01-30-CGO-LLVM.html]]. In CGO ’04: Proceedings of the International Symposium on Code Generation and Optimization: Feedback-directed and Runtime Optimization, 2004.
- Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. [[Formalizing the LLVM Intermediate Representation for Verified Program Transformations|http://www.cis.upenn.edu/~jianzhou/Vellvm/]]. In POPL ’12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages,
- LLVM Related Publications page on llvm.org
- Projects:
- UFO - an LLVM-based framework for verifying (and finding bugs in) sequential C programs
- PAGAI - an LLVM-based static analyser based on abstract interpretation
- bugst - a collection of C++ libraries providing static program analyses
- CPAchecker - a configurable software verification tool
- SMACK - a LLVM-based static checker of properties of programs written in C/C++