Related work

On this page, you can find:

• Alternative formal methods
• Variants/subsets of C/C++ that aim at safety
• Parsing C++
• Programming-language semantics

Static 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.

SLAM project [paper] (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 [paper] [paper] (Jeff Foster)

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.

CCured: 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.

Proof-Carrying Code (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.

Translation 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++

Larch/C++ is an interface-specification and behavioral-specification language for C++.

Software robots [Tech report]

Rösch Consulting, a German company, promises bug-free programs by way of generating source code from specifications.

``Strict 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.

Safe, 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 implementation details.

Cyclone [Paper] [Paper] (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 on.

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).

RC [paper] (David Gay)

A dialect of C that adds safe, region-based memory management to C.

Vault [paper]

A C-like language that was created in a spirit similar to Cyclone.

Safe C [Techreport] (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] [PS] (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.

Embedded C++ (EC++)

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.

C#

A language derived from C++ with supposedly more strictly defined semantics

Managed Extensions for C++ [web]

Microsoft's port of C++ to its Common Language Environment, a virtual machine for multiple programming languages

Programming Research's QA C, QA C++

A tool that can detect violations of a C/C++ subset specification

Discussion 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 for C++.''

Software that includes a C++ parser

• OpenC++ is a compile-time introspection tool for ISO C++. It contains an easy-to-understand ad-hoc recursive-descent parser.
• PCCTS-based 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.
• FOG, a meta-compiler (preprocessor) for C++.
• Keystone, an object-oriented C++ parser with symbol-table construction (see paper below); avaliable for research purposes
• Sage++, a compiler-preprocessor toolkit for refactoring.
• PUMA, a source-code transformation system
• Vortex, a compiler infrastructure
• CInt, a C/C++ interpreter
• Cmm, a C++ extension for multimethods
• GCC, the GNU Compiler Collection. CVS branch "cp-parser-branch" has a new, recursive-descent parser.
• TenDRA, another open-source C/C++ compiler
  • Info on Parsing C++ in TenDRA.
• Sandro Sigala's yaccable C/C++ grammars, without symbol-table resolution

Introduction To Parsing C++

An overview of the various work on parsing C++, some of which also appears below.

Evolving Object-Oriented Designs with Refactorings (Lance A. Tokuda)

A dissertation on refactoring that, among other things, describes Sage++.

Meta-Compilation 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 symbol-table construction.

A Generated Parser of C++ (Warwick Irvin, Neville Churcher)

Proposes using a Tomita parser to parse C++.

A parser for the C language written in SML (Chris Toshok, Luke Sheneman, James Alves-Foss)

Parsing C++ Despite Missing Declarations

The semantics of the C++ programming language (Charles Wallace)

C formalized in HOL (Michael Norrish) [Review of Dennis Ritchie + newsgroup discussion]

Denotational Semantics of ANSI C (Nikolaos S. Papaspyrou)

SPARK [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.''