Demo 2:  Software analysis and verification in practice
               Marius Minea

Techniques bridging static analysis and formal methods have evolved
to the point where they can effectively diagnose potential problems in
system functionality, or offer exhaustive correctness guarantees.
We present some public-domain tools that are practically applicable
to either large-scale systems or selected critical fragments:
- the Splint static analysis tool, which detects problems such as
buffer overflows, uninitialized variables or null dereferences in C code
- the Spin verifier, specialized for communication protocols and C code
- the Bandera verification toolkit for Java programs
- the BLAST software verification system for C programs
We also discuss our experience in implementing custom analyses for
diagnosing specific problems in software systems.