Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/ ZENODOarrow_drop_down
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Report . 2022
License: CC BY
Data sources: Datacite
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Report . 2022
License: CC BY
Data sources: ZENODO
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Report . 2022
License: CC BY
Data sources: ZENODO
versions View all 3 versions
addClaim

This Research product is the result of merged Research products in OpenAIRE.

You have already added 0 works in your ORCID record related to the merged Research product.

Circular lists in Iris ∗ deduction rules of ▷

Authors: Bergwerf, Herman;

Circular lists in Iris ∗ deduction rules of ▷

Abstract

One concern of theoretical computer science is to prove the correctness of algorithms, for example the implementation of datastructures that are at the core of almost all programs. This becomes especially complicated when concurrency is involved in a non-trivial way, such that multiple parts of memory that logically belong together are modified in parallel. Proof Assistants are computer programs that enable logical reasoning in a strict formal proof system. Developing proofs inside a such a proof assistant requires extreme rigour. As long as your definitions are not flawed, it is practically impossible to miss edge cases. The proof assistant we use is called Coq. Coq is not readily usable to reason about programs that use mutable resources, but the Iris project has built a framework inside Coq that offers a convenient language and toolbox for this. Iris uses separation logic and modal logic to reason about memory, concurrency, and potentially non-terminating recursion. Contributions: Circular lists in Iris We formalize a circular doubly linked list in Coq/Iris using separation logic. We only verified synchronous list operations. This chapter demonstrates the use of separation logic to reason about locations stored on a heap. To our knowledge this is the first interactive verification of a circular list using separation logic. Deduction rules of ��� We study the model of plain step-indexed propositions without resources, a basic interpretation of the ��� modality. We determine a complete set of deductions, and formalize an algorithm that checks a finite number of potential counterexamples in Coq, proving decidability and completeness.

Keywords

separation logic, formal verification, modal logic

14 references, page 1 of 2

[1] [4] [5] [6] [7] [2] J. Richard Büchi. “Weak Second-Order Arithmetic and Finite Automata”. In: Mathematical Logic Quarterly 6.1-6 (1960), pp. 66-92. doi: https: //doi.org/10.1002/malq.19600060105.

[3] Saul A. Kripke. “Semantical Analysis of Intuitionistic Logic I”. In: Formal Systems and Recursive Functions. Ed. by J.N. Crossley and M.A.E. Dummett. Vol. 40. Studies in Logic and the Foundations of Mathematics. Elsevier, 1965, pp. 92-130. doi: 10.1016/S0049-237X(08)71685-9. [OpenAIRE]

C. A. R. Hoare. “An Axiomatic Basis for Computer Programming”. In: Commun. ACM 12.10 (Oct. 1969), pp. 576-580. issn: 0001-0782. doi: 10.1145/363235.363259.

In: Machine intelligence 7.91-99 (1972), p. 300.

Alexander Chagrov and Michael Zakharyashchev. “The Disjunction Property of Intermediate Propositional Logics”. In: Studia Logica: An International Journal for Symbolic Logic 50.2 (1991), pp. 189-216. issn: 00393215, 15728730. url: http://www.jstor.org/stable/20015573.

Alexandre Boudet and Hubert Comon. “Diophantine equations, Presburger arithmetic and finite automata”. In: Trees in Algebra and Programming - CAAP '96. Ed. by Hélène Kirchner. Berlin, Heidelberg: Springer Berlin Heidelberg, 1996, pp. 30-43. isbn: 978-3-540-49944-2.

[8] Jacob Elgaard, Nils Klarlund, and Anders Møller. “MONA 1.x: New Techniques for WS1S and WS2S”. English. In: Computer Aided Verification . Ed. by Alan J. Hu and Moshe Y. Vardi. Lecture Notes in Computer Science. 10th International Conference on Computer Aided Verification. CAV 1998 ; Conference date: 28-06-1998 Through 02-07-1998. Netherlands: Springer, 1998, pp. 516-520. doi: 10.1007/BFb0028773. [OpenAIRE]

Hiroshi Nakano. “Fixed-Point Logic with the Approximation Modality and Its Kripke Completeness”. In: Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software. TACS '01. Berlin, Heidelberg: Springer-Verlag, 2001, pp. 165-182. isbn: 3540427368.

[13] J.C. Reynolds. “Separation logic: a logic for shared mutable data structures”. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. 2002, pp. 55-74. doi: 10.1109/LICS.2002.1029817.

[11] John C. Reynolds. “Intuitionistic Reasoning about Shared Mutable Data Structure”. In: Millennial Perspectives in Computer Science. Palgrave, 2000, pp. 303-321.

  • BIP!
    Impact byBIP!
    citations
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    0
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
    OpenAIRE UsageCounts
    Usage byUsageCounts
    visibility views 327
    download downloads 90
  • citations
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    0
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
    Powered byBIP!BIP!
  • 327
    views
    90
    downloads
    Powered byOpenAIRE UsageCounts
Powered by OpenAIRE graph
Found an issue? Give us feedback
visibility
download
citations
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
views
OpenAIRE UsageCountsViews provided by UsageCounts
downloads
OpenAIRE UsageCountsDownloads provided by UsageCounts
0
Average
Average
Average
327
90
Green