Show simple item record

dc.contributor.authorNkounkou, Brittany
dc.date.accessioned2021-03-12T17:38:55Z
dc.date.available2021-03-12T17:38:55Z
dc.date.issued2020-08
dc.identifier.otherNkounkou_cornellgrad_0058F_12173
dc.identifier.otherhttp://dissertations.umi.com/cornellgrad:12173
dc.identifier.urihttps://hdl.handle.net/1813/102911
dc.description83 pages
dc.descriptionSupplemental file(s) description: Coq Code.
dc.description.abstractCorrectness and trust in a piece of software is important, especially for complex and/or critical systems like medical devices, computerized weapons, or any management of private data. Certified software aims to evidence correctness and establish trust in software by pairing executable instructions with mechanically-verifiable proofs that certain properties of the instructions are upheld. In this dissertation, we build certified software that is used to design asynchronous circuits. These circuits differ from synchronous circuits by coordinating communication via local message-passing channels rather than a global clock signal. Asynchronous circuits improve upon the time- and power-efficiency of synchronous circuits, but also introduce the complexity challenges of decentralized circuit communication. Communicating Hardware Processes (CHP) is a language used to write high-level asynchronous circuit designs. We use the Coq Proof Assistant to build a mechanical formalization of CHP language semantics and a certified CHP program simulator. The semantics formalization is novel in the combination of its mechanization, its comprehensive expression of the CHP language, and its precise abstraction of lower-level circuit design decisions. The simulator is novel in its certification, which mechanically verifies that it simulates a CHP program correctly, and it serves as a model for future Coq-built CHP software tools that can be certified against the mechanical language semantics.
dc.language.isoen
dc.rightsAttribution-ShareAlike 4.0 International
dc.rights.urihttps://creativecommons.org/licenses/by-sa/4.0/
dc.subjectasynchronous circuits
dc.subjectcertified software
dc.subjectcommunicating hardware processes
dc.subjectcoq proof assistant
dc.subjectformal methods
dc.subjectprogramming languages
dc.titleCertified Software for Designing Asynchronous Circuits
dc.typedissertation or thesis
thesis.degree.disciplineComputer Science
thesis.degree.grantorCornell University
thesis.degree.levelDoctor of Philosophy
thesis.degree.namePh. D., Computer Science
dc.contributor.chairTate, Ross Everett
dc.contributor.committeeMemberManohar, Rajit
dc.contributor.committeeMemberWeatherspoon, Hakim
dc.contributor.committeeMemberConstable, Bob
dcterms.licensehttps://hdl.handle.net/1813/59810
dc.identifier.doihttps://doi.org/10.7298/c9ar-j170


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Except where otherwise noted, this item's license is described as Attribution-ShareAlike 4.0 International

Statistics