## Abstract / Description of output

This paper focuses on the important, but tricky, problem of determining

provably correct program properties automatically from program source. We

describe a novel approach to constructing correct low-level programs. By using

modern, full-spectrum dependent types, we are able to give an explicit and checkable

link between the low-level program and its high-level meaning. Our approach

closely links programming and theorem proving in that a type correct program is a

constructive proof that the program meets its specification. It goes beyond typical

model-checking approaches, that are commonly used to check formal properties

of low-level programs, by building proofs over abstractions of properties. In this

way, we avoid the state-space explosion problem that bedevils model-checking

solutions. We are also able to consider properties over potentially infinite domains

and determine properties for potentially infinite programs. We illustrate

our approach by implementing a carry-ripple adder for binary numbers.

provably correct program properties automatically from program source. We

describe a novel approach to constructing correct low-level programs. By using

modern, full-spectrum dependent types, we are able to give an explicit and checkable

link between the low-level program and its high-level meaning. Our approach

closely links programming and theorem proving in that a type correct program is a

constructive proof that the program meets its specification. It goes beyond typical

model-checking approaches, that are commonly used to check formal properties

of low-level programs, by building proofs over abstractions of properties. In this

way, we avoid the state-space explosion problem that bedevils model-checking

solutions. We are also able to consider properties over potentially infinite domains

and determine properties for potentially infinite programs. We illustrate

our approach by implementing a carry-ripple adder for binary numbers.

Original language | English |
---|---|

Title of host publication | Proceedings of the Eighth Symposium on Trends in Functional Programming, TFP 2007, New York City, New York, USA, April 2-4. 2007. |

Pages | 159-176 |

Number of pages | 18 |

DOIs | |

Publication status | Published - 2007 |