View in EDS PDF Full Text

Co-Developing Programs and Their Proof of Correctness.

Saved in:
Bibliographic Details
Title: Co-Developing Programs and Their Proof of Correctness.
Authors: Chapman, Roderick1 (AUTHOR) rodchap@amazon.co.uk, Dross, Claire2 (AUTHOR), Matthews, Stuart3 (AUTHOR), Moy, Yannick2 (AUTHOR)
Source: Communications of the ACM. Mar2024, Vol. 67 Issue 3, p84-94. 11p.
Subjects: SPARK (Computer program language), Programming languages, Electronic data processing, Computer programming, Computer software development, Computer software correctness
Abstract: The article focuses on the auto-active approach for co-developing programs and their proof of correctness, specifically the open source SPARK technology. The authors discuss the key design and technological choices for SPARK, which made it successful within the industry, and explore the possible future of SPARK and other analyzers of the same family.
Database: Engineering Source
FullText Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 175599200
AccessLevel: 6
PubType: Periodical
PubTypeId: serialPeriodical
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Co-Developing Programs and Their Proof of Correctness.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Chapman%2C+Roderick%22">Chapman, Roderick</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> rodchap@amazon.co.uk</i><br /><searchLink fieldCode="AR" term="%22Dross%2C+Claire%22">Dross, Claire</searchLink><relatesTo>2</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Matthews%2C+Stuart%22">Matthews, Stuart</searchLink><relatesTo>3</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Moy%2C+Yannick%22">Moy, Yannick</searchLink><relatesTo>2</relatesTo> (AUTHOR)
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Communications+of+the+ACM%22">Communications of the ACM</searchLink>. Mar2024, Vol. 67 Issue 3, p84-94. 11p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22SPARK+%28Computer+program+language%29%22">SPARK (Computer program language)</searchLink><br /><searchLink fieldCode="DE" term="%22Programming+languages%22">Programming languages</searchLink><br /><searchLink fieldCode="DE" term="%22Electronic+data+processing%22">Electronic data processing</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+programming%22">Computer programming</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software+development%22">Computer software development</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software+correctness%22">Computer software correctness</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: The article focuses on the auto-active approach for co-developing programs and their proof of correctness, specifically the open source SPARK technology. The authors discuss the key design and technological choices for SPARK, which made it successful within the industry, and explore the possible future of SPARK and other analyzers of the same family.
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=175599200
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1145/3624728
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 11
        StartPage: 84
    Subjects:
      – SubjectFull: SPARK (Computer program language)
        Type: general
      – SubjectFull: Programming languages
        Type: general
      – SubjectFull: Electronic data processing
        Type: general
      – SubjectFull: Computer programming
        Type: general
      – SubjectFull: Computer software development
        Type: general
      – SubjectFull: Computer software correctness
        Type: general
    Titles:
      – TitleFull: Co-Developing Programs and Their Proof of Correctness.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Chapman, Roderick
      – PersonEntity:
          Name:
            NameFull: Dross, Claire
      – PersonEntity:
          Name:
            NameFull: Matthews, Stuart
      – PersonEntity:
          Name:
            NameFull: Moy, Yannick
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 03
              Text: Mar2024
              Type: published
              Y: 2024
          Identifiers:
            – Type: issn-print
              Value: 00010782
          Numbering:
            – Type: volume
              Value: 67
            – Type: issue
              Value: 3
          Titles:
            – TitleFull: Communications of the ACM
              Type: main
ResultId 1