View in EDS

Formalization of a Parameterized Parallel Adder within the Coq Theorem Prover.

Saved in:
Bibliographic Details
Title: Formalization of a Parameterized Parallel Adder within the Coq Theorem Prover.
Authors: Gang Chen1 gang.chen@lingcore.com
Source: IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems. Jan2010, Vol. 29 Issue 1, p149-153. 5p. 1 Graph.
Subjects: Parallel computer program verification, Computer arithmetic, Formal methods (Computer science), Parameter estimation, Integrated circuits
Abstract: This paper describes a new advancement in theorem proving based formal verification: a formalization of a parameterized parallel prefix adder developed in the proof assistant Coq. [ABSTRACT FROM AUTHOR]
Copyright of IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems is the property of IEEE and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 47935798
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Formalization of a Parameterized Parallel Adder within the Coq Theorem Prover.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Gang+Chen%22">Gang Chen</searchLink><relatesTo>1</relatesTo><i> gang.chen@lingcore.com</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22IEEE+Transactions+on+Computer-Aided+Design+of+Integrated+Circuits+%26+Systems%22">IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems</searchLink>. Jan2010, Vol. 29 Issue 1, p149-153. 5p. 1 Graph.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Parallel+computer+program+verification%22">Parallel computer program verification</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+arithmetic%22">Computer arithmetic</searchLink><br /><searchLink fieldCode="DE" term="%22Formal+methods+%28Computer+science%29%22">Formal methods (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Parameter+estimation%22">Parameter estimation</searchLink><br /><searchLink fieldCode="DE" term="%22Integrated+circuits%22">Integrated circuits</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: This paper describes a new advancement in theorem proving based formal verification: a formalization of a parameterized parallel prefix adder developed in the proof assistant Coq. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems is the property of IEEE and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=47935798
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1109/TCAD.2009.2034346
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 5
        StartPage: 149
    Subjects:
      – SubjectFull: Parallel computer program verification
        Type: general
      – SubjectFull: Computer arithmetic
        Type: general
      – SubjectFull: Formal methods (Computer science)
        Type: general
      – SubjectFull: Parameter estimation
        Type: general
      – SubjectFull: Integrated circuits
        Type: general
    Titles:
      – TitleFull: Formalization of a Parameterized Parallel Adder within the Coq Theorem Prover.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Gang Chen
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 01
              Text: Jan2010
              Type: published
              Y: 2010
          Identifiers:
            – Type: issn-print
              Value: 02780070
          Numbering:
            – Type: volume
              Value: 29
            – Type: issue
              Value: 1
          Titles:
            – TitleFull: IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems
              Type: main
ResultId 1