-
Tracing the Origins of Verification Conditions
The typical program verification system is a batch tool that accepts as input a program annotated with Floyd-Hoare assertions, performs syntactic and semantic analysis... -
Reasoning with Executable Specifications
Starting from the specification of a small imperative programming language, and the description of two program transformations on this language, we formally prove the... -
Towards a Generic Trace for Rule Based Constraint Reasoning
CHR is a very versatile programming language that allows programmers to declaratively specify constraint solvers. An important part of the development of such solvers... -
Programming Language Specifications and Environments
These are course notes on programming language formal descriptions and their use to build programming environments and to prove properties of these languages. -
AS, for Abstract Syntax Manual - V1.0
This is the manual for AS, an abstract syntax specification formalism. The main features of this formalism are modularity and support for second-order abstract...
