View source for Publications:A Methodology for Generating Verified Combinatorial Circuits

<div style='display: none'>
== Do not edit this section ==
</div>
{{PublicationSetupTemplate|Author=Oleg Kiselyov, Kedar N. Swadi, Walid Taha
|PID=588274
|Name=Kiselyov, Oleg (Fleet Numerical Meteorology and Oceanography Center, Monterey, CA 93943);Swadi, Kedar N. (Department of Computer Science Rice University);Taha, Walid [waltah] (Department of Computer Science Rice University)
|Title=A Methodology for Generating Veriﬁed Combinatorial Circuits
|PublicationType=Conference Paper
|ContentType=Refereegranskat
|Language=eng
|Journal=
|JournalISSN=
|Status=
|Volume=
|Issue=
|HostPublication=
|Conference=EMSOFT'04. International Conference on Embedded Software and Systems.
|StartPage=
|EndPage=
|Year=2004
|Edition=
|Pages=
|City=
|Publisher=
|Series=
|SeriesISSN=
|ISBN=
|Urls=
|ISRN=
|DOI=
|ISI=
|PMID=
|ScopusId=
|NBN=urn:nbn:se:hh:diva-20975
|LocalId=
|ArchiveNumber=
|Keywords=Multi-stage programming;abstract interpretation
|Categories=Datorsystem (20206)
|ResearchSubjects=
|Projects=
|Notes=
|Abstract=<p>High-level programming languages offer signiﬁcant expressivitybut provide little or no guarantees about resource use. Resourcebounded languages — such as hardware-description languages —provide strong guarantees about the runtime behavior of computations but often lack mechanisms that allow programmers to writemore structured, modular, and reusable programs. To overcomethis basic tension in language design, recent work advocated the useof Resource-aware Programming (RAP) languages, which take intoaccount the natural distinction between the development platformand the deployment platform for resource-constrained software.This paper investigates the use of RAP languages for the generation of combinatorial circuits. The key challenge that we encounteris that the RAP approach does not safely admit a mechanism to express a posteriori (post-generation) optimizations. The paper proposes and studies the use of abstract interpretation to overcome thisproblem. The approach is illustrated using an in-depth analysis ofthe Fast Fourier Transform (FFT). The generated computations arecomparable to those generated by FFTW.</p>
|Opponents=
|Supervisors=
|Examiners=
|Patent=
|ThesisLevel=
|Credits=
|Programme=
|Subject=
|Uppsok=
|DefencePlace=
|DefenceLanguage=
|DefenceDate=
|CreatedDate=2013-01-14
|PublicationDate=2013-01-15
|LastUpdated=2014-01-24
|diva=http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:588274}}
<div style='display: none'>

== Keep all hand-made modifications below ==
</div>{{PublicationDisplayTemplate}}