View in EDS

Concise outlines for a complex logic: a proof outline checker for TaDA.

Saved in:
Bibliographic Details
Title: Concise outlines for a complex logic: a proof outline checker for TaDA.
Authors: Wolf, Felix A.1 (AUTHOR) felix.wolf@inf.ethz.ch, Schwerhoff, Malte1 (AUTHOR), Müller, Peter1 (AUTHOR)
Source: Formal Methods in System Design. Aug2022, Vol. 61 Issue 1, p110-136. 27p.
Subjects: Logic, Software verification, Checkers
Abstract: Modern separation logics allow one to prove rich properties of intricate code, e.g., functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics difficult to apply. Manual proofs or proofs in interactive theorem provers consist of a large number of steps, often with subtle side conditions. On the other hand, automation with dedicated verifiers typically requires sophisticated proof search algorithms that are specific to the given program logic, resulting in limited tool support that makes it difficult to experiment with program logics, e.g., when learning, improving, or comparing them. Proof outline checkers fill this gap. Their input is a program annotated with the most essential proof steps, just like the proof outlines typically presented in papers. The tool then checks automatically that this outline represents a valid proof in the program logic. In this paper, we systematically develop a proof outline checker for the TaDA logic, which reduces the checking to a simpler verification problem, for which automated tools exist. Our approach leads to proof outline checkers that provide substantially more automation than interactive provers, but are much simpler to develop than custom automatic verifiers. [ABSTRACT FROM AUTHOR]
Copyright of Formal Methods in System Design is the property of Springer Nature 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: 173923487
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Concise outlines for a complex logic: a proof outline checker for TaDA.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Wolf%2C+Felix+A%2E%22">Wolf, Felix A.</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> felix.wolf@inf.ethz.ch</i><br /><searchLink fieldCode="AR" term="%22Schwerhoff%2C+Malte%22">Schwerhoff, Malte</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Müller%2C+Peter%22">Müller, Peter</searchLink><relatesTo>1</relatesTo> (AUTHOR)
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Formal+Methods+in+System+Design%22">Formal Methods in System Design</searchLink>. Aug2022, Vol. 61 Issue 1, p110-136. 27p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Logic%22">Logic</searchLink><br /><searchLink fieldCode="DE" term="%22Software+verification%22">Software verification</searchLink><br /><searchLink fieldCode="DE" term="%22Checkers%22">Checkers</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Modern separation logics allow one to prove rich properties of intricate code, e.g., functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics difficult to apply. Manual proofs or proofs in interactive theorem provers consist of a large number of steps, often with subtle side conditions. On the other hand, automation with dedicated verifiers typically requires sophisticated proof search algorithms that are specific to the given program logic, resulting in limited tool support that makes it difficult to experiment with program logics, e.g., when learning, improving, or comparing them. Proof outline checkers fill this gap. Their input is a program annotated with the most essential proof steps, just like the proof outlines typically presented in papers. The tool then checks automatically that this outline represents a valid proof in the program logic. In this paper, we systematically develop a proof outline checker for the TaDA logic, which reduces the checking to a simpler verification problem, for which automated tools exist. Our approach leads to proof outline checkers that provide substantially more automation than interactive provers, but are much simpler to develop than custom automatic verifiers. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Formal Methods in System Design is the property of Springer Nature 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=173923487
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s10703-023-00427-w
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 27
        StartPage: 110
    Subjects:
      – SubjectFull: Logic
        Type: general
      – SubjectFull: Software verification
        Type: general
      – SubjectFull: Checkers
        Type: general
    Titles:
      – TitleFull: Concise outlines for a complex logic: a proof outline checker for TaDA.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Wolf, Felix A.
      – PersonEntity:
          Name:
            NameFull: Schwerhoff, Malte
      – PersonEntity:
          Name:
            NameFull: Müller, Peter
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 08
              Text: Aug2022
              Type: published
              Y: 2022
          Identifiers:
            – Type: issn-print
              Value: 09259856
          Numbering:
            – Type: volume
              Value: 61
            – Type: issue
              Value: 1
          Titles:
            – TitleFull: Formal Methods in System Design
              Type: main
ResultId 1