Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types

Edwin Brady, James McKinna, Kevin Hammond

Research output: Contribution to conferencePaper

Abstract

This paper focuses on the important, but tricky, problem of determiningprovably correct program properties automatically from program source. Wedescribe a novel approach to constructing correct low-level programs. By usingmodern, full-spectrum dependent types, we are able to give an explicit and checkablelink between the low-level program and its high-level meaning. Our approachclosely links programming and theorem proving in that a type correct program is aconstructive proof that the program meets its specification. It goes beyond typicalmodel-checking approaches, that are commonly used to check formal propertiesof low-level programs, by building proofs over abstractions of properties. In thisway, we avoid the state-space explosion problem that bedevils model-checkingsolutions. We are also able to consider properties over potentially infinite domainsand determine properties for potentially infinite programs. We illustrateour approach by implementing a carry-ripple adder for binary numbers.
Original languageEnglish
Pages159-176
Number of pages18
Publication statusPublished - 2007
Event8th Symposium on Trends in Functional Programming 2007 - New York City, United States
Duration: 2 Apr 20074 Apr 2007

Conference

Conference8th Symposium on Trends in Functional Programming 2007
Abbreviated titleTFP 2007
CountryUnited States
CityNew York City
Period2/04/074/04/07

Fingerprint Dive into the research topics of 'Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types'. Together they form a unique fingerprint.

  • Cite this

    Brady, E., McKinna, J., & Hammond, K. (2007). Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types. 159-176. Paper presented at 8th Symposium on Trends in Functional Programming 2007, New York City, United States.