Static Analysis with Goanna - Using model checking to analyze large code bases. PDF slides
Ansgar Fehnker
National Information and Communications Technology in Australia

10/22/10, 2 PM, GHC-6501


Goanna is a source code analysis tool that uses a combination of static analysis tools and model checking to analyze C/C++ code bases. In this talk I will introduce the concept of syntactic model checking that lies at the heart of Goanna. In it a very coarse abstraction of the source code is annotated with syntactic information which allows to model check many traditional static analysis properties. Furthermore I will discuss ongoing work on model checking for recursive Kripke Structures, a technique that can be used to check source code inter-procedurally.


Ansgar Fehnker is senior researcher at National ICT Australia. He is currently involved in two research projects, one that combines static analysis and model checking and applies this to C/C++ source code, and one that look as timed and probabilistic verification techniques, and then applied to wireless mesh networks.

 Ansgar Fehnker holds a PhD in Computer Science at the University of Nijmegen in the field of verification of timed and hybrid systems. He was a visiting researcher with ECE and CS at Carnegie Mellon University, Pittsburgh, before he joined NICTA in 2004.

Content for class "clear" Goes Here
nsfSupported by an Expeditions in Computing award from the National Science Foundation