**UsageCounts**

Found an issue? Give us feedback

Please grant OpenAIRE to access and update your ORCID works.

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.

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

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.

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

All Research products

```
<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=undefined&type=result"></script>');
-->
</script>
```

For further information contact us at __helpdesk@openaire.eu__

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

separation logic, formal verification, modal logic

[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.

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 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!- 327views90downloads

Found an issue? Give us feedback

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).

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.

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).

Influence provided by **BIP!**

impulse

This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.

Impulse provided by **BIP!**

views

Views provided by **UsageCounts**

downloads

Downloads provided by **UsageCounts**

0

Average

Average

Average

327

90

Green