View in EDS

A verified Common Lisp implementation of Buchberger’s algorithm in ACL2

Saved in:
Bibliographic Details
Title: A verified Common Lisp implementation of Buchberger’s algorithm in ACL2
Authors: Medina-Bulo, Inmaculada1 http://neptuno.uca.es/~inmame, Palomo-Lozano, Francisco1 http://neptuno.uca.es/~palomo, Ruiz-Reina, José-Luis2 http://www.cs.us.es/~jruiz
Source: Journal of Symbolic Computation. Jan2010, Vol. 45 Issue 1, p96-123. 28p.
Subjects: COMMON LISP (Computer program language), Algorithms, ACL (Computer program language), Polynomials, Programming languages, Software verification, Algebra software
Abstract: Abstract: In this article, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides an integrated environment where programming (in a pure functional subset of Common Lisp) and formal verification of programs, with the assistance of a theorem prover, are possible. Our implementation is written in a real programming language and it is directly executable within the ACL2 system or any compliant Common Lisp system. We provide here snippets of real verified code, discuss the formalization details in depth, and present quantitative data about the proof effort. [Copyright &y& Elsevier]
Copyright of Journal of Symbolic Computation is the property of Academic Press Inc. 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: 44483773
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: A verified Common Lisp implementation of Buchberger’s algorithm in ACL2
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Medina-Bulo%2C+Inmaculada%22">Medina-Bulo, Inmaculada</searchLink><relatesTo>1</relatesTo><i> http://neptuno.uca.es/~inmame</i><br /><searchLink fieldCode="AR" term="%22Palomo-Lozano%2C+Francisco%22">Palomo-Lozano, Francisco</searchLink><relatesTo>1</relatesTo><i> http://neptuno.uca.es/~palomo</i><br /><searchLink fieldCode="AR" term="%22Ruiz-Reina%2C+José-Luis%22">Ruiz-Reina, José-Luis</searchLink><relatesTo>2</relatesTo><i> http://www.cs.us.es/~jruiz</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Journal+of+Symbolic+Computation%22">Journal of Symbolic Computation</searchLink>. Jan2010, Vol. 45 Issue 1, p96-123. 28p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22COMMON+LISP+%28Computer+program+language%29%22">COMMON LISP (Computer program language)</searchLink><br /><searchLink fieldCode="DE" term="%22Algorithms%22">Algorithms</searchLink><br /><searchLink fieldCode="DE" term="%22ACL+%28Computer+program+language%29%22">ACL (Computer program language)</searchLink><br /><searchLink fieldCode="DE" term="%22Polynomials%22">Polynomials</searchLink><br /><searchLink fieldCode="DE" term="%22Programming+languages%22">Programming languages</searchLink><br /><searchLink fieldCode="DE" term="%22Software+verification%22">Software verification</searchLink><br /><searchLink fieldCode="DE" term="%22Algebra+software%22">Algebra software</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Abstract: In this article, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides an integrated environment where programming (in a pure functional subset of Common Lisp) and formal verification of programs, with the assistance of a theorem prover, are possible. Our implementation is written in a real programming language and it is directly executable within the ACL2 system or any compliant Common Lisp system. We provide here snippets of real verified code, discuss the formalization details in depth, and present quantitative data about the proof effort. [Copyright &y& Elsevier]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Journal of Symbolic Computation is the property of Academic Press Inc. 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=44483773
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1016/j.jsc.2009.07.002
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 28
        StartPage: 96
    Subjects:
      – SubjectFull: COMMON LISP (Computer program language)
        Type: general
      – SubjectFull: Algorithms
        Type: general
      – SubjectFull: ACL (Computer program language)
        Type: general
      – SubjectFull: Polynomials
        Type: general
      – SubjectFull: Programming languages
        Type: general
      – SubjectFull: Software verification
        Type: general
      – SubjectFull: Algebra software
        Type: general
    Titles:
      – TitleFull: A verified Common Lisp implementation of Buchberger’s algorithm in ACL2
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Medina-Bulo, Inmaculada
      – PersonEntity:
          Name:
            NameFull: Palomo-Lozano, Francisco
      – PersonEntity:
          Name:
            NameFull: Ruiz-Reina, José-Luis
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 01
              Text: Jan2010
              Type: published
              Y: 2010
          Identifiers:
            – Type: issn-print
              Value: 07477171
          Numbering:
            – Type: volume
              Value: 45
            – Type: issue
              Value: 1
          Titles:
            – TitleFull: Journal of Symbolic Computation
              Type: main
ResultId 1