Links to related projects:
Links and Resources
Open Source links:
- Software Quality Courses: There were two associated Software
Quality courses offered in 2001 at Berkeley.
course covered program analysis, model checking and theorem
proving in some depth.
course was a broader survey of software quality issues.
new C-like programming language that enforces programmer specified API
rules. Device drivers are one example of a domain that can benefit from
Software, Languages, Analysis and Model checking research group.
MONA: The MONA project at BRICS: it
decides monadic second-order logic statements.
PALE: The Pointer Assertion Logic
project at BRICS: it uses the MONA project to reason about the behavior of
programs that use pointers.
(Compaq) SRC's Extended Static Checking project.
JML: The Java
Modeling Language (JML) is a behavioral interface specification language
that can be used to specify the behavior of Java modules. It combines the
approaches of Eiffel and Larch, with some elements of the refinement
is a multi-site project exploring methods, languages, and tools for the
practical use of formal specifications. Here's what some
researchers at Compaq SRC had to say
"We did our first experiments using the Larch prover. Since this prover
requires human guidance to find a proof, the programmer had to guide the
prover through a proof, and an error would be revealed by the failure of
the process. Damien Doligez found a locking error in auto-flush writers
using this prover, but for mere mortals it is too laborious to be
LCLint: A static checker for
C that makes use of source code annotations (part of the Larch project).
Gimpel Software: A C/C++
static checker that looks across multiple modules.
Bandera: A Kansas
State project using software model construction for finite-state
verification of Java.
- Lande: A
project at IRISA with a central focus on automated tools that aid
development and logical validation. The tools aim for a strong grounding
in language semantics and security models. Lots of stuff on Prolog and
Slicing, but their annotated LaTeX bibliography
is quite useful.
- Agitar: Automated testing for
- Parasoft: Parasoft's Insure++
product does run-time checking through source code modification. Their
CodeWizard tool does static checking to make sure that C/C++ code adheres
to generic and user-defined coding styles and library interfaces. Jin Kim
is willing to give us 3 day trial-licenses of these products for comparison
with our tools and research. Email
me if you would like to try them out.
- Flawfinder: A C/C++
static checker for security flaws.
A selected bibliography of related research
papers is available. (This page is out of date.)
Related research papers:
Page maintained by Joel Galenson.