static analysis you say?

[ge at linuxbox.org (Gadi Evron)]

Just last month Greta Yorsh, fresh from work in Microsoft Research over 
in the US lectured to us on something related in TAUSEC 
(http://www.cs.tau.ac.il/tausec - in Hebrew).

-----
Title: Testing, Abstraction, Theorem Proving: Better Together.

We present a method for static program analysis that leverages tests
and concrete program executions.  State abstractions generalizes the
set of program states obtained from concrete executions.  A theorem
prover is then used for checking that the generalized set of concrete
states covers all potential executions, and
satisfies additional safety properties.

Our method finds the same potential errors as the most-precise abstract
interpreter for a given abstraction, and potentially more efficient.
Additionally, it provides a new
way to tune performance by alternating between concrete execution and
theorem proving.
-----

Anyone follow that? I didn't.

VERY basically put, she showed a system that was developed over 5 years 
that abstracts static code such as of device drivers to a simple boolean 
program, and then follows the code to find errors. Later comparing these 
errors to a run on a tad less abstracted program to see if the error is 
really there.

^^^ That is probably the worst description you will ever hear of SLAM.

She claims that with her research (not SLAM) she can prove 
mathematically a program is secure.. erm. She was a very impressive 
lecturer and almost convinced me, I really was impressed.

Here are some links from her lecture (ignore the first line which is in 
Hebrew):
http://www.cs.tau.ac.il/tausec/lectures/Greta_Yorsh_links.html

        Gadi.