SAML is a framework for static analysis written in Standard ML, a statically typed functional language. In its complete form, SAML is intended to provide a framework that will facilitate the formulation of analyses on a program's abstract syntax tree. It does this by providing higher order functions which apply operations across the AST.
This semester we are integrating SAML with KAT-ML theorem prover developed by Kamal Aboul-Hosn and Dexter Kozen. KAT-ML is a Standard ML based theorem prover for Kleene Algebra with Tests. Our goal is for SAML to develop a set of conjectures about an input program, which can proven by KAT-ML. For example, SAML would identify excecution paths with potential null-pointer deferences, and ask KAT-ML to show that program logic prevents these deferences from actually occuring.
This research is being conducted under the guidance of Profressor Dexter Kozen of Cornell University.
Download Haakon Larsen's SAML report.