(* = offsite link)
On this page, we provide an (mostly unsorted) collection links to
related projects and publications. Please find a more formal review
of related work in our techical report Applying source-code verification to a
microkernel - The VFiasco project.
On this page, you can find:
Alternative formal methods
debugging of C programs: detection of pointer errors in recursive
data structures (Ronan Gaugne)
- Describes a static analyzer for C that checks static assertions
in C code. This analyzer uses operational semantics to
formalize the C code.
(Thomas Ball, Sriram K. Rajamani)
- ``Our goal is to be able to check that software satisfies
critical behavioral properties of the interfaces it uses, and to aid
software engineers in designing interfaces and software to ensure
reliable and correct functioning.''
This tool uses model checking to verify predicates of a boolean
program generated from a C program.
- cqual is a
type-based analysis tool for finding bugs in C programs. cqual
extends the type system of C with extra user-defined type
qualifiers. The programmer annotates their program in a few places,
and cqual performs qualifier inference to check whether the
annotations are correct.
Type-Safe Retrofitting of Legacy Code
(George C. Necula, Scott McPeak, Westley Weimer)
- Extends C with a new type system that separates pointers
according to their usage. The CCured system then allows
pointers that can be statically verified to be type safe, and
inserts runtime checks for other pointer uses.
(George C. Necula)
- Proposes delivering compiled code together with a proof that
establishes that the code complies to a given security policy.
The proofs can be validated automatically and inexpensively by
a simple proof checker.
Part of the project is the development of Touchstone,
a certifying compiler [paper]
that automatically generates type-correctness proofs for Java.
Validation for an Optimizing Compiler
(George C. Necula)
- Translation validation is a promising technique that proposes
to verify the correctness of each compilation as is happens.
- Larch/C++ is an interface-specification and
behavioral-specification language for C++.
- Rösch Consulting, a German company, promises bug-free programs
by way of generating source code from specifications.
Variants/subsets of C/C++ that aim at safety
Mode'' for C++
- John Nagle proposes an extension to C++ that aims at preventing
dangling pointers: When taking the address of an automatic
variable, the pointer that holds the address (``auto
pointer'') needs to be of
lesser scope than the variable.
Efficient Garbage Collection for C++ (John R. Ellis and
David L. Detlefs)
- This paper discusses a safe subset of C++ that uses garbage
collection and weak pointers, including a discussion on
(Trevor Jim, Greg Morrisett, et al)
- Cyclone is a programming language based on C that is safe,
meaning that it rules out programs that have buffer overflows,
dangling pointers, format string attacks, and so
Cyclone offers either garbage collection and
region-based memory management, but currently no
user-controlled memory management. Region-based memory
management seems to be similar to John Nagle's ``auto
pointers'' in his ``Strict Mode for C++'' (see above).
- A dialect of C that adds safe, region-based memory management
- A C-like language that was created in a spirit similar to Cyclone.
- Safe C
(Todd Austin, Scott Breach, Gurindar Sohi)
- Proposes using a smart pointer to catch all temporal and spatial
pointer-access errors at runtime. This proposal requires no
modification of the base language.
- C++ in
Safety Critical Systems [HTML]
(David W. Binkley)
- A number of guidelines that apply a general set of guidelines
for safety-critical software to C++.
- Safer C
- In his book, Les Hatton proposes a coding standard that aims at avoiding
common errors in C programming.
- MISRA C
- A subset of C that aims at avoiding
common errors in C programming.
- A subset of C++ for embedded systems. (Is safety a goal here?)
- Internet C++
- Defines a virtual machine for C++ with fixed integer sizes and
fixed OS APIs. Internet C++ programs do not need to be ported
-- only the virtual machine needs porting.
- A language derived from C++ with supposedly more strictly
Extensions for C++
- Microsoft's port of C++ to its Common Language Environment, a
virtual machine for multiple programming languages
Research's QA C, QA C++
- A tool that can detect violations of a C/C++ subset specification
on C++ safety
[Related postings in comp.lang.c++.moderated]
- ``It is my understanding that the European Railway signalling
standard is seriously considering the use of C++ in SIL4-type
applications [SIL = Safety Integrity Level]. I regard this as a
serious mistake since the language is not defined precisely
enough. I would like to know your views!''
``It is not clear that there can be a well-defined semantics
- Software that includes a C++ parser
is a compile-time introspection tool for ISO C++. It
contains an easy-to-understand ad-hoc recursive-descent parser.
embeddable C++ parser. This is an ISO C++ parser
library based on the PCCTS parser generator.
- GCC_XML, a
GCC extension that outputs parsed C++ in an XML format.
a meta-compiler (preprocessor) for C++.
- Keystone, an object-oriented C++ parser with
symbol-table construction (see paper below); avaliable
for research purposes
a compiler-preprocessor toolkit for refactoring.
- PUMA, a
source-code transformation system
a compiler infrastructure
- CInt, a
- Cmm, a C++
extension for multimethods
- GCC, the GNU Compiler
Collection. CVS branch "cp-parser-branch" has a new,
another open-source C/C++ compiler
Sigala's yaccable C/C++ grammars, without
To Parsing C++
- An overview of the various work on parsing C++, some of which
also appears below.
Object-Oriented Designs with Refactorings (Lance A. Tokuda)
- A dissertation on refactoring that, among other things,
for C++ (Edward D. Willink)
- A dissertation that describes FOG. This work descends quite
deeply into the ugliness of C++ parsing.
- Symbol Table
Construction and Name Lookup in ISO C++ (James
F. Power, Brian A. Malloy)
- Describes Keystone, an object-oriented C++ parser with
Generated Parser of C++ (Warwick Irvin, Neville Churcher)
- Proposes using a Tomita parser to parse C++.
parser for the C language written in SML
(Chris Toshok, Luke Sheneman, James Alves-Foss)
C++ Despite Missing Declarations
semantics of the C++ programming language (Charles
formalized in HOL (Michael Norrish)
[Review of Dennis Ritchie + newsgroup discussion]
Semantics of ANSI C (Nikolaos S. Papaspyrou)
[Posting by Rod Chapman]
``1) SPARK ("The SPADE Ada Kernel") is an annotated subset of Ada that is
appropriate for the construction of high-integrity systems.
2) The static analysis tool is called the Examiner - it does static semantic
checking, data- and information-flow analysis and verification condition
generation. There's also a theorem prover and proof checker for discharging
those VCs if need be.''
``One thing I forgot to mention earlier - the definition of SPARK (both
83 and 95 variants) and the formal semantics of SPARK83 are freely
available to anyone that wants them. I think these should be required
reading for anyone studying language design! See www.sparkada.com.''
Last modified: Wed Jun 14 09:54:12 2006