Links and Resources

• Software Quality Courses: There were two associated Software Quality courses offered in 2001 at Berkeley. The spring course covered program analysis, model checking and theorem proving in some depth. The fall course was a broader survey of software quality issues.
• Vault: Microsoft's new C-like programming language that enforces programmer specified API rules. Device drivers are one example of a domain that can benefit from this approach.
• SLAM: Microsoft's 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.
• ESC: DEC (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 calculus.
• Larch: Larch 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 about Larch:

  "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 practical."

• 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 Java.
• 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.

• Tux.Org: Tux.Org is an umbrella organization supporting the efforts of Linux Users Groups and Developers.
• Kernel.Org: This is the primary site for the Linux kernel source, but it has much more than just kernels.
• Secure Programming for Linux and Unix HOWTO: A freely-available book on how to write secure software on Linux and Unix.
• Kernel Traffic & Cousins: Linux Kernel Traffic and the Cousins are an attempt to track the activities of various developer mailing lists.
• Redhat Device Driver News: An old Redhat message board about Linux device drivers with a resource section.
• The Linux Kernel: A book describing the 2.0.33 Linux Kernel sources. It is an overview of the Kernel structure with little or no information on APIs.
• Linux Kernel Module Programming Guide: A Rubini-like book that apparently covers 2.2 kernels.
• The Linux-Kernel Archive: An archive of email traffic on the linux-kernel mailing list.
• The Linux-Kernel Mailing List FAQ: Actually a very general Linux and Linux documentation FAQ.
• Linux Device Drivers: The website for Alessandro Rubini's book.
• Freefire Project: Support for developers of free security solutions.

Related research papers:

Page maintained by Joel Galenson.