Log in

Relevant bibliographies by topics / Separation logic / Journal articles

Journal articles on the topic 'Separation logic'

To see the other types of publications on this topic, follow the link: Separation logic.

Author: Grafiati

Published: 4 June 2021

Last updated: 25 May 2024

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles

Select a source type:

Consult the top 50 journal articles for your research on the topic 'Separation logic.'

Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.

You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.

Browse journal articles on a wide variety of disciplines and organise your bibliography correctly.

1

Demri, Stéphane, and Raul Fervari. "The power of modal separation logics." Journal of Logic and Computation 29, no. 8 (December 2019): 1139–84. http://dx.doi.org/10.1093/logcom/exz019.

Full text

Abstract:

Abstract We introduce a modal separation logic MSL whose models are memory states from separation logic and the logical connectives include modal operators as well as separating conjunction and implication from separation logic. With such a combination of operators, some fragments of MSL can be seen as genuine modal logics whereas some others capture standard separation logics, leading to an original language to speak about memory states. We analyse the decidability status and the computational complexity of several fragments of MSL, obtaining surprising results by design of proof methods that take into account the modal and separation features of MSL. For example, the satisfiability problem for the fragment of MSL with $\Diamond $, the difference modality $\langle \neq \rangle $ and separating conjunction $\ast $ is shown Tower-complete whereas the restriction either to $\Diamond $ and $\ast $ or to $\langle \neq \rangle $ and $\ast $ is only NP-complete. We establish that the full logic MSL admits an undecidable satisfiability problem. Furthermore, we investigate variants of MSL with alternative semantics and we build bridges with interval temporal logics and with logics equipped with sabotage operators.

APA, Harvard, Vancouver, ISO, and other styles

2

O'Hearn, Peter. "Separation logic." Communications of the ACM 62, no. 2 (January 28, 2019): 86–95. http://dx.doi.org/10.1145/3211968.

Full text

APA, Harvard, Vancouver, ISO, and other styles

3

Dardinier, Thibault, Peter Müller, and Alexander J. Summers. "Fractional resources in unbounded separation logic." Proceedings of the ACM on Programming Languages 6, OOPSLA2 (October 31, 2022): 1066–92. http://dx.doi.org/10.1145/3563326.

Full text

Abstract:

Many separation logics support fractional permissions to distinguish between read and write access to a heap location, for instance, to allow concurrent reads while enforcing exclusive writes. Fractional permissions extend to composite assertions such as (co)inductive predicates and magic wands by allowing those to be multiplied by a fraction. Typical separation logic proofs require that this multiplication has three key properties: it needs to distribute over assertions, it should permit fractions to be factored out from assertions, and two fractions of the same assertion should be combinable into one larger fraction. Existing formal semantics incorporating fractional assertions into a separation logic define multiplication semantically (via models), resulting in a semantics in which distributivity and combinability do not hold for key resource assertions such as magic wands, and fractions cannot be factored out from a separating conjunction. By contrast, existing automatic separation logic verifiers define multiplication syntactically, resulting in a different semantics for which it is unknown whether distributivity and combinability hold for all assertions. In this paper, we present a novel semantics for separation logic assertions that allows states to hold more than a full permission to a heap location during the evaluation of an assertion. By reimposing upper bounds on the permissions held per location at statement boundaries, we retain key properties of separation logic, in particular, the frame rule. Our assertion semantics unifies semantic and syntactic multiplication and thereby reconciles the discrepancy between separation logic theory and tools and enjoys distributivity, factorisability, and combinability. We have formalised our semantics and proved its properties in Isabelle/HOL.

APA, Harvard, Vancouver, ISO, and other styles

4

Brookes, Stephen, and Peter W. O'Hearn. "Concurrent separation logic." ACM SIGLOG News 3, no. 3 (August 8, 2016): 47–65. http://dx.doi.org/10.1145/2984450.2984457.

Full text

APA, Harvard, Vancouver, ISO, and other styles

5

Vafeiadis, Viktor, and Chinmay Narayan. "Relaxed separation logic." ACM SIGPLAN Notices 48, no. 10 (November 12, 2013): 867–84. http://dx.doi.org/10.1145/2544173.2509532.

Full text

APA, Harvard, Vancouver, ISO, and other styles

6

Yang, Hongseok. "Relational separation logic." Theoretical Computer Science 375, no. 1-3 (May 2007): 308–34. http://dx.doi.org/10.1016/j.tcs.2006.12.036.

Full text

APA, Harvard, Vancouver, ISO, and other styles

7

Dang, H. H., P. Höfner, and B. Möller. "Algebraic separation logic." Journal of Logic and Algebraic Programming 80, no. 6 (August 2011): 221–47. http://dx.doi.org/10.1016/j.jlap.2011.04.003.

Full text

APA, Harvard, Vancouver, ISO, and other styles

8

Courtault, J. R., H. van Ditmarsch, and D. Galmiche. "A public announcement separation logic." Mathematical Structures in Computer Science 29, no. 06 (April 15, 2019): 828–71. http://dx.doi.org/10.1017/s0960129518000348.

Full text

Abstract:

AbstractWe define a Public Announcement Separation Logic (PASL) that allows us to consider epistemic possible worlds as resources that can be shared or separated, in the spirit of separation logics. After studying its semantics and illustrating its interest for modelling systems, we provide a sound and complete tableau calculus that deals with resource, agent and announcement constraints and give also a countermodel extraction method.

APA, Harvard, Vancouver, ISO, and other styles

9

Demri, Stéphane, Etienne Lozes, and Alessio Mansutti. "The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic." ACM Transactions on Computational Logic 22, no. 2 (June 21, 2021): 1–56. http://dx.doi.org/10.1145/3448269.

Full text

Abstract:

The list segment predicate ls used in separation logic for verifying programs with pointers is well suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating conjunction and implication, which is motivated by the recent design of new fragments in which all these ingredients are used indifferently and verification tools start to handle the magic wand connective. This is a very natural extension that has not been studied so far. We show that the restriction without the separating implication can be solved in polynomial space by using an appropriate abstraction for memory states, whereas the full extension is shown undecidable by reduction from first-order separation logic. Many variants of the logic and fragments are also investigated from the computational point of view when ls is added, providing numerous results about adding reachability predicates to quantifier-free separation logic.

APA, Harvard, Vancouver, ISO, and other styles

10

Timany, Amin, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, and Lars Birkedal. "Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement." Proceedings of the ACM on Programming Languages 8, POPL (January 5, 2024): 241–72. http://dx.doi.org/10.1145/3632851.

Full text

Abstract:

Expressive state-of-the-art separation logics rely on step-indexing to model semantically complex features and to support modular reasoning about imperative higher-order concurrent and distributed programs. Step- indexing comes, however, with an inherent cost: it restricts the adequacy theorem of program logics to a fairly simple class of safety properties. In this paper, we explore if and how intensional refinement is a viable methodology for strengthening higher-order concurrent (and distributed) separation logic to prove non-trivial safety and liveness properties. Specifically, we introduce Trillium, a language-agnostic separation logic framework for showing intensional refinement relations between traces of a program and a model. We instantiate Trillium with a concurrent language and develop Fairis, a concurrent separation logic, that we use to show liveness properties of concurrent programs under fair scheduling assumptions through a fair liveness-preserving refinement of a model. We also instantiate Trillium with a distributed language and obtain an extension of Aneris, a distributed separation logic, which we use to show refinement relations between distributed systems and TLA+ models.

APA, Harvard, Vancouver, ISO, and other styles

11

Bao, Jialu, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti. "A separation logic for negative dependence." Proceedings of the ACM on Programming Languages 6, POPL (January 16, 2022): 1–29. http://dx.doi.org/10.1145/3498719.

Full text

Abstract:

Formal reasoning about hashing-based probabilistic data structures often requires reasoning about random variables where when one variable gets larger (such as the number of elements hashed into one bucket), the others tend to be smaller (like the number of elements hashed into the other buckets). This is an example of negative dependence , a generalization of probabilistic independence that has recently found interesting applications in algorithm design and machine learning. Despite the usefulness of negative dependence for the analyses of probabilistic data structures, existing verification methods cannot establish this property for randomized programs. To fill this gap, we design LINA, a probabilistic separation logic for reasoning about negative dependence. Following recent works on probabilistic separation logic using separating conjunction to reason about the probabilistic independence of random variables, we use separating conjunction to reason about negative dependence. Our assertion logic features two separating conjunctions, one for independence and one for negative dependence. We generalize the logic of bunched implications (BI) to support multiple separating conjunctions, and provide a sound and complete proof system. Notably, the semantics for separating conjunction relies on a non-deterministic , rather than partial, operation for combining resources. By drawing on closure properties for negative dependence, our program logic supports a Frame-like rule for negative dependence and monotone operations. We demonstrate how LINA can verify probabilistic properties of hash-based data structures and balls-into-bins processes.

APA, Harvard, Vancouver, ISO, and other styles

12

Raad, Azalea, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn. "Concurrent incorrectness separation logic." Proceedings of the ACM on Programming Languages 6, POPL (January 16, 2022): 1–29. http://dx.doi.org/10.1145/3498695.

Full text

Abstract:

Incorrectness separation logic (ISL) was recently introduced as a theory of under-approximate reasoning, with the goal of proving that compositional bug catchers find actual bugs. However, ISL only considers sequential programs. Here, we develop concurrent incorrectness separation logic (CISL), which extends ISL to account for bug catching in concurrent programs. Inspired by the work on Views, we design CISL as a parametric framework, which can be instantiated for a number of bug catching scenarios, including race detection, deadlock detection, and memory safety error detection. For each instance, the CISL meta-theory ensures the soundness of incorrectness reasoning for free, thereby guaranteeing that the bugs detected are true positives.

APA, Harvard, Vancouver, ISO, and other styles

13

Parkinson, Matthew, and Gavin Bierman. "Separation logic and abstraction." ACM SIGPLAN Notices 40, no. 1 (January 12, 2005): 247–58. http://dx.doi.org/10.1145/1047659.1040326.

Full text

APA, Harvard, Vancouver, ISO, and other styles

14

Pym, David, Jonathan M. Spring, and Peter O’Hearn. "Why Separation Logic Works." Philosophy & Technology 32, no. 3 (May 22, 2018): 483–516. http://dx.doi.org/10.1007/s13347-018-0312-8.

Full text

APA, Harvard, Vancouver, ISO, and other styles

15

Barthe, Gilles, Justin Hsu, and Kevin Liao. "A probabilistic separation logic." Proceedings of the ACM on Programming Languages 4, POPL (January 2020): 1–30. http://dx.doi.org/10.1145/3371123.

Full text

APA, Harvard, Vancouver, ISO, and other styles

16

Dang, Han-Hing, and Bernhard B. Möller. "Extended transitive separation logic." Journal of Logical and Algebraic Methods in Programming 84, no. 3 (May 2015): 303–25. http://dx.doi.org/10.1016/j.jlamp.2014.12.002.

Full text

APA, Harvard, Vancouver, ISO, and other styles

17

Soares, Pedro, António Ravara, and Simão Melo de Sousa. "Revisiting concurrent separation logic." Journal of Logical and Algebraic Methods in Programming 89 (June 2017): 41–66. http://dx.doi.org/10.1016/j.jlamp.2017.02.004.

Full text

APA, Harvard, Vancouver, ISO, and other styles

18

Gregersen, Simon Oddershede, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. "Asynchronous Probabilistic Couplings in Higher-Order Separation Logic." Proceedings of the ACM on Programming Languages 8, POPL (January 5, 2024): 753–84. http://dx.doi.org/10.1145/3632868.

Full text

Abstract:

Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational program logics, this manifests as dedicated coupling rules that, e.g., say we may reason as if two sampling statements return the same value. However, this approach fundamentally requires aligning or "synchronizing" the sampling statements of the two programs which is not always possible. In this paper, we develop Clutch, a higher-order probabilistic relational separation logic that addresses this issue by supporting asynchronous probabilistic couplings. We use Clutch to develop a logical step-indexed logical relation to reason about contextual refinement and equivalence of higher-order programs written in a rich language with a probabilistic choice operator, higher-order local state, and impredicative polymorphism. Finally, we demonstrate our approach on a number of case studies. All the results that appear in the paper have been formalized in the Coq proof assistant using the Coquelicot library and the Iris separation logic framework.

APA, Harvard, Vancouver, ISO, and other styles

19

Spies, Simon, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. "Later credits: resourceful reasoning for the later modality." Proceedings of the ACM on Programming Languages 6, ICFP (August 29, 2022): 283–311. http://dx.doi.org/10.1145/3547631.

Full text

Abstract:

In the past two decades, step-indexed logical relations and separation logics have both come to play a major role in semantics and verification research. More recently, they have been married together in the form of step-indexed separation logics like VST, iCAP, and Iris, which provide powerful tools for (among other things) building semantic models of richly typed languages like Rust. In these logics, propositions are given semantics using a step-indexed model, and step-indexed reasoning is reflected into the logic through the so-called “later” modality. On the one hand, this modality provides an elegant, high-level account of step-indexed reasoning; on the other hand, when used in sufficiently sophisticated ways, it can become a nuisance, turning perfectly natural proof strategies into dead ends. In this work, we introduce later credits , a new technique for escaping later-modality quagmires. By leveraging the second ancestor of these logics—separation logic—later credits turn “the right to eliminate a later” into an ownable resource, which is subject to all the traditional modular reasoning principles of separation logic. We develop the theory of later credits in the context of Iris, and present several challenging examples of proofs and proof patterns which were previously not possible in Iris but are now possible due to later credits.

APA, Harvard, Vancouver, ISO, and other styles

20

Parkinson, Matthew J., and Gavin M. Bierman. "Separation logic, abstraction and inheritance." ACM SIGPLAN Notices 43, no. 1 (January 14, 2008): 75–86. http://dx.doi.org/10.1145/1328897.1328451.

Full text

APA, Harvard, Vancouver, ISO, and other styles

21

Bornat, Richard, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. "Permission accounting in separation logic." ACM SIGPLAN Notices 40, no. 1 (January 12, 2005): 259–70. http://dx.doi.org/10.1145/1047659.1040327.

Full text

APA, Harvard, Vancouver, ISO, and other styles

22

Tuch, Harvey, Gerwin Klein, and Michael Norrish. "Types, bytes, and separation logic." ACM SIGPLAN Notices 42, no. 1 (January 17, 2007): 97–108. http://dx.doi.org/10.1145/1190215.1190234.

Full text

APA, Harvard, Vancouver, ISO, and other styles

23

Tan, Gang, Zhong Shao, Xinyu Feng, and Hongxu Cai. "Weak Updates and Separation Logic." New Generation Computing 29, no. 1 (January 2011): 3–29. http://dx.doi.org/10.1007/s00354-010-0097-5.

Full text

APA, Harvard, Vancouver, ISO, and other styles

24

Wehrman, Ian, C. A. R. Hoare, and Peter W. O'Hearn. "Graphical models of separation logic." Information Processing Letters 109, no. 17 (August 2009): 1001–4. http://dx.doi.org/10.1016/j.ipl.2009.06.003.

Full text

APA, Harvard, Vancouver, ISO, and other styles

25

Luo, Chenguang, and Shengchao Qin. "Separation Logic for Multiple Inheritance." Electronic Notes in Theoretical Computer Science 212 (April 2008): 27–40. http://dx.doi.org/10.1016/j.entcs.2008.04.051.

Full text

APA, Harvard, Vancouver, ISO, and other styles

26

Tuch, Harvey. "Structured Types and Separation Logic." Electronic Notes in Theoretical Computer Science 217 (July 2008): 41–59. http://dx.doi.org/10.1016/j.entcs.2008.06.041.

Full text

APA, Harvard, Vancouver, ISO, and other styles

27

Bao, Yuyan, Gary T. Leavens, and Gidon Ernst. "Unifying separation logic and region logic to allow interoperability." Formal Aspects of Computing 30, no. 3-4 (May 25, 2018): 381–441. http://dx.doi.org/10.1007/s00165-018-0455-5.

Full text

APA, Harvard, Vancouver, ISO, and other styles

28

Song, Youngju, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer. "Conditional Contextual Refinement." Proceedings of the ACM on Programming Languages 7, POPL (January 9, 2023): 1121–51. http://dx.doi.org/10.1145/3571232.

Full text

Abstract:

Much work in formal verification of low-level systems is based on one of two approaches: refinement or separation logic. These two approaches have complementary benefits: refinement supports the use of programs as specifications, as well as transitive composition of proofs, whereas separation logic supports conditional specifications, as well as modular ownership reasoning about shared state. A number of verification frameworks employ these techniques in tandem, but in all such cases the benefits of the two techniques remain separate. For example, in frameworks that use relational separation logic to prove contextual refinement, the relational separation logic judgment does not support transitive composition of proofs, while the contextual refinement judgment does not support conditional specifications. In this paper, we propose Conditional Contextual Refinement (or CCR, for short), the first verification system to not only combine refinement and separation logic in a single framework but also to truly marry them together into a unified mechanism enjoying all the benefits of refinement and separation logic simultaneously. Specifically, unlike in prior work, CCR’s refinement specifications are both conditional (with separation logic pre- and post-conditions) and transitively composable. We implement CCR in Coq and evaluate its effectiveness on a range of interesting examples.

APA, Harvard, Vancouver, ISO, and other styles

29

Bugaieva, Liudmyla, and Yurii Beznosyk. "Heuristic procedure for synthesis of separation system for multicomponent mixtures using fuzzy logic." Proceedings of the NTUU “Igor Sikorsky KPI”. Series: Chemical engineering, ecology and resource saving, no. 1 (March 29, 2022): 44–54. http://dx.doi.org/10.20535/2617-9741.1.2022.254158.

Full text

Abstract:

In this study, the task is to develop a heuristic procedure for the synthesis of systems for the separation of multicomponent mixtures, which would take into account the uncertainty of the factors of the separation processes and the multivariance of the solution. The authors reviewed the current state of the existing methods for the separation of mixtures. Many works devoted to the synthesis of effective systems for the separation of multicomponent mixtures leave unsolved the problem of taking into account the uncertainty of many factors of the separation processes. In the presented work, it is proposed that a heuristic approach is applied using fuzzy logic. The proposed procedure is based on the choice of a separation sequence that takes into account the value of the separation coefficient and the difference in boiling points of two adjacent key components. The proposed strategy is based on an estimate of the likelihood of each rule for each possible separation. The search for solutions has five stages. First, the mixture to be separated and the available equipment are determined. After that, an ordered list of all separation options is drawn up with possible values of the economic costs of their implementation. Next, the mass load of possible separation is estimated and the separation with the minimum value of the separation ratio is selected. The heuristic is that the heavy separation is done last. And, at the last step, the most economical separation scheme is selected. The above strategy at the stage of quantitative assessment is subject to the value of the threshold S (boiling point difference). This point can be used to determine the quasi-optimal solutions to the problem of sequencing according to the rules of relaxation of separation. For this fuzzy heuristic method for determining cost-effective separation sequences for mixtures, appropriate software has been developed. In addition, since the procedure uses the theory of fuzzy sets, the Fuzzy Logic Toolbox package of the Matlab was also used to solve the problem of synthesizing schemes for separating hydrocarbon mixtures. The proposed procedure was successfully tested in both software implementations using the example of separating a five-component mixture. The main difference between the proposed approach and other approaches based on fuzzy logic for the synthesis of separation systems is the gradation of working rules and possible quantification of a set of rules, which eliminates conflicts between the rules.

APA, Harvard, Vancouver, ISO, and other styles

30

Birkedal, Lars, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. "Theorems for free from separation logic specifications." Proceedings of the ACM on Programming Languages 5, ICFP (August 22, 2021): 1–29. http://dx.doi.org/10.1145/3473586.

Full text

Abstract:

Separation logic specifications with abstract predicates intuitively enforce a discipline that constrains when and how calls may be made between a client and a library. Thus a separation logic specification of a library intuitively enforces a protocol on the trace of interactions between a client and the library. We show how to formalize this intuition and demonstrate how to derive "free theorems" about such interaction traces from abstract separation logic specifications. We present several examples of free theorems. In particular, we prove that a so-called logically atomic concurrent separation logic specification of a concurrent module operation implies that the operation is linearizable. All the results presented in this paper have been mechanized and formally proved in the Coq proof assistant using the Iris higher-order concurrent separation logic framework.

APA, Harvard, Vancouver, ISO, and other styles

31

Li, John M., Amal Ahmed, and Steven Holtzen. "Lilac: A Modal Separation Logic for Conditional Probability." Proceedings of the ACM on Programming Languages 7, PLDI (June 6, 2023): 148–71. http://dx.doi.org/10.1145/3591226.

Full text

Abstract:

We present Lilac, a separation logic for reasoning about probabilistic programs where separating conjunction captures probabilistic independence. Inspired by an analogy with mutable state where sampling corresponds to dynamic allocation, we show how probability spaces over a fixed, ambient sample space appear to be the natural analogue of heap fragments, and present a new combining operation on them such that probability spaces behave like heaps and measurability of random variables behaves like ownership. This combining operation forms the basis for our model of separation, and produces a logic with many pleasant properties. In particular, Lilac has a frame rule identical to the ordinary one, and naturally accommodates advanced features like continuous random variables and reasoning about quantitative properties of programs. Then we propose a new modality based on disintegration theory for reasoning about conditional probability. We show how the resulting modal logic validates examples from prior work, and give a formal verification of an intricate weighted sampling algorithm whose correctness depends crucially on conditional independence structure.

APA, Harvard, Vancouver, ISO, and other styles

32

ZAPLETAL, JINDŘICH. "SEPARATION PROBLEMS AND FORCING." Journal of Mathematical Logic 13, no. 01 (May 28, 2013): 1350002. http://dx.doi.org/10.1142/s0219061313500025.

Full text

Abstract:

Certain separation problems in descriptive set theory correspond to a forcing preservation property, with a fusion type infinite game associated to it. As an application, it is consistent with the axioms of set theory that the circle 𝕋 can be covered by ℵ1 many closed sets of uniqueness while a much larger number of H-sets is necessary to cover it.

APA, Harvard, Vancouver, ISO, and other styles

33

Galmiche, Didier, and Daniel Méry. "Labelled cyclic proofs for separation logic." Journal of Logic and Computation 31, no. 3 (April 2021): 892–922. http://dx.doi.org/10.1093/logcom/exab017.

Full text

Abstract:

Abstract Separation logic (SL) is a logical formalism for reasoning about programs that use pointers to mutate data structures. It is successful for program verification as an assertion language to state properties about memory heaps using Hoare triples. Most of the proof systems and verification tools for ${\textrm{SL}}$ focus on the decidable but rather restricted symbolic heaps fragment. Moreover, recent proof systems that go beyond symbolic heaps are purely syntactic or labelled systems dedicated to some fragments of ${\textrm{SL}}$ and they mainly allow either the full set of connectives, or the definition of arbitrary inductive predicates, but not both. In this work, we present a labelled proof system, called ${\textrm{G}_{\textrm{SL}}}$, that allows both the definition of cyclic proofs with arbitrary inductive predicates and the full set of SL connectives. We prove its soundness and show that we can derive in ${\textrm{G}_{\textrm{SL}}}$ the built-in rules for data structures of another non-cyclic labelled proof system and also that ${\textrm{G}_{\textrm{SL}}}$ is strictly more powerful than that system.

APA, Harvard, Vancouver, ISO, and other styles

34

Blom, Stefan, Saeed Darabi, and Marieke Huisman. "Verifying Parallel Loops with Separation Logic." Electronic Proceedings in Theoretical Computer Science 155 (June 12, 2014): 47–53. http://dx.doi.org/10.4204/eptcs.155.7.

Full text

APA, Harvard, Vancouver, ISO, and other styles

35

de Vilhena, Paulo Emílio, and François Pottier. "A separation logic for effect handlers." Proceedings of the ACM on Programming Languages 5, POPL (January 4, 2021): 1–28. http://dx.doi.org/10.1145/3434314.

Full text

APA, Harvard, Vancouver, ISO, and other styles

36

Vafeiadis, Viktor. "Concurrent Separation Logic and Operational Semantics." Electronic Notes in Theoretical Computer Science 276 (September 2011): 335–51. http://dx.doi.org/10.1016/j.entcs.2011.09.029.

Full text

APA, Harvard, Vancouver, ISO, and other styles

37

Kapoor, Kalpesh, Kamal Lodaya, and Uday S. Reddy. "Fine-grained Concurrency with Separation Logic." Journal of Philosophical Logic 40, no. 5 (May 21, 2011): 583–632. http://dx.doi.org/10.1007/s10992-011-9195-1.

Full text

APA, Harvard, Vancouver, ISO, and other styles

38

Brookes, Stephen. "A semantics for concurrent separation logic." Theoretical Computer Science 375, no. 1-3 (May 2007): 227–70. http://dx.doi.org/10.1016/j.tcs.2006.12.034.

Full text

APA, Harvard, Vancouver, ISO, and other styles

39

Winterstein, Felix J., Samuel R. Bayliss, and George A. Constantinides. "Separation Logic for High-Level Synthesis." ACM Transactions on Reconfigurable Technology and Systems 9, no. 2 (February 3, 2016): 1–23. http://dx.doi.org/10.1145/2836169.

Full text

APA, Harvard, Vancouver, ISO, and other styles

40

Demri, Stéphane, Didier Galmiche, Dominique Larchey-Wendling, and Daniel Méry. "Separation Logic with One Quantified Variable." Theory of Computing Systems 61, no. 2 (May 31, 2017): 371–461. http://dx.doi.org/10.1007/s00224-016-9713-1.

Full text

APA, Harvard, Vancouver, ISO, and other styles

41

Bornat, Richard, Cristiano Calcagno, and Hongseok Yang. "Variables as Resource in Separation Logic." Electronic Notes in Theoretical Computer Science 155 (May 2006): 247–76. http://dx.doi.org/10.1016/j.entcs.2005.11.059.

Full text

APA, Harvard, Vancouver, ISO, and other styles

42

Hoare, Tony, and Peter O'Hearn. "Separation Logic Semantics for Communicating Processes." Electronic Notes in Theoretical Computer Science 212 (April 2008): 3–25. http://dx.doi.org/10.1016/j.entcs.2008.04.050.

Full text

APA, Harvard, Vancouver, ISO, and other styles

43

Meyer, Roland, Thomas Wies, and Sebastian Wolff. "Embedding Hindsight Reasoning in Separation Logic." Proceedings of the ACM on Programming Languages 7, PLDI (June 6, 2023): 1848–71. http://dx.doi.org/10.1145/3591296.

Full text

Abstract:

Automatically proving linearizability of concurrent data structures remains a key challenge for verification. We present temporal interpolation as a new proof principle to guide automated proof search using hindsight arguments within concurrent separation logic. Temporal interpolation offers an easy-to-automate alternative to prophecy variables and has the advantage of structuring proofs into easy-to-discharge hypotheses. Additionally, we advance hindsight theory by integrating it into a program logic, bringing formal rigor and complementary proof machinery. We substantiate the usefulness of temporal interpolation by implementing it in a tool and using it to automatically verify the Logical Ordering tree. The proof is challenging due to future-dependent linearization points and complex structure overlays. It is the first formal proof of this data structure. Interestingly, our formalization revealed an unknown bug and an existing informal proof as erroneous.

APA, Harvard, Vancouver, ISO, and other styles

44

Fullilove, Mindy Thompson. "Escaping the Catastrophic Logic of Separation." Health Equity 7, no. 1 (January 1, 2023): 53–60. http://dx.doi.org/10.1089/heq.2022.29021.mtf.

Full text

APA, Harvard, Vancouver, ISO, and other styles

45

Moine, Alexandre, Sam Westrick, and Stephanie Balzer. "DisLog: A Separation Logic for Disentanglement." Proceedings of the ACM on Programming Languages 8, POPL (January 5, 2024): 302–31. http://dx.doi.org/10.1145/3632853.

Full text

Abstract:

Disentanglement is a run-time property of parallel programs that facilitates task-local reasoning about the memory footprint of parallel tasks. In particular, it ensures that a task does not access any memory locations allocated by another concurrently executing task. Disentanglement can be exploited, for example, to implement a high-performance parallel memory manager, such as in the MPL (MaPLe) compiler for Parallel ML. Prior research on disentanglement has focused on the design of optimizations, either trusting the programmer to provide a disentangled program or relying on runtime instrumentation for detecting and managing entanglement. This paper provides the first static approach to verify that a program is disentangled: it contributes DisLog, a concurrent separation logic for disentanglement. DisLog enriches concurrent separation logic with the notions necessary for reasoning about the fork-join structure of parallel programs, allowing the verification that memory accesses are effectively disentangled. A large class of programs, including race-free programs, exhibit memory access patterns that are disentangled "by construction". To reason about these patterns, the paper distills from DisLog an almost standard concurrent separation logic, called DisLog+. In this high-level logic, no specific reasoning about memory accesses is needed: functional correctness proofs entail disentanglement. The paper illustrates the use of DisLog and DisLog+ on a range of case studies, including two different implementations of parallel deduplication via concurrent hashing. All our results are mechanized in the Coq proof assistant using Iris.

APA, Harvard, Vancouver, ISO, and other styles

46

Dardinier, Thibault, Gaurav Parthasarathy, and Peter Müller. "Verification-Preserving Inlining in Automatic Separation Logic Verifiers." Proceedings of the ACM on Programming Languages 7, OOPSLA1 (April 6, 2023): 789–818. http://dx.doi.org/10.1145/3586054.

Full text

Abstract:

Bounded verification has proved useful to detect bugs and to increase confidence in the correctness of a program. In contrast to unbounded verification, reasoning about calls via (bounded) inlining and about loops via (bounded) unrolling does not require method specifications and loop invariants and, therefore, reduces the annotation overhead to the bare minimum, namely specifications of the properties to be verified. For verifiers based on traditional program logics, verification is preserved by inlining (and unrolling): successful unbounded verification of a program w.r.t. some annotation implies successful verification of the inlined program. That is, any error detected in the inlined program reveals a true error in the original program. However, this essential property might not hold for automatic separation logic verifiers such as Caper, GRASShopper, RefinedC, Steel, VeriFast, and verifiers based on Viper. In this setting, inlining generally changes the resources owned by method executions, which may affect automatic proof search algorithms and introduce spurious errors. In this paper, we present the first technique for verification-preserving inlining in automatic separation logic verifiers. We identify a semantic condition on programs and prove in Isabelle/HOL that it ensures verification-preserving inlining for state-of-the-art automatic separation logic verifiers. We also prove a dual result: successful verification of the inlined program ensures that there are method and loop annotations that enable the verification of the original program for bounded executions. To check our semantic condition automatically, we present two approximations that can be checked syntactically and with a program verifier, respectively. We implement these checks in Viper and demonstrate that they are effective for non-trivial examples from different verifiers.

APA, Harvard, Vancouver, ISO, and other styles

47

Kondratyev, Dmitry A. "Logic for reasoning about bugs in loops over data sequences (IFIL)." Modeling and Analysis of Information Systems 30, no. 3 (September 17, 2023): 214–33. http://dx.doi.org/10.18255/1818-1015-2023-3-214-233.

Full text

Abstract:

Classic deductive verification is not focused on reasoning about program incorrectness. Reasoning about program incorrectness using formal methods is an important problem nowadays. Special logics such as Incorrectness Logic, Adversarial Logic, Local Completeness Logic, Exact Separation Logic and Outcome Logic have recently been proposed to address it. However, these logics have two disadvantages. One is that they are based on under-approximation approaches, while classic deductive verification is based on the over-approximation approach. One the other hand, the use of the classic approach requires defining loop invariants in a general case. The second disadvantage is that the use of generalized inference rules from these logics results in having to prove too complex formulas in simple cases. Our contribution is a new logic for solving these problems in the case of loops over data sequences. These loops are referred to as finite iterations. We call the proposed logic the Incorrectness Finite Iteration Logic (IFIL). We avoid defining invariants of finite iterations using a symbolic replacement of these loops with recursive functions. Our logic is based on special inference rules for finite iterations. These rules allow generating formulas with recursive functions corresponding to finite iterations. The validity of these formulas may indicate the presence of bugs in the finite iterations. This logic has been implemented in a new version of the C-lightVer system for deductive verification of C programs.

APA, Harvard, Vancouver, ISO, and other styles

48

Vindum, Simon Friis, and Lars Birkedal. "Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory." Proceedings of the ACM on Programming Languages 7, OOPSLA2 (October 16, 2023): 632–57. http://dx.doi.org/10.1145/3622820.

Full text

Abstract:

Weak persistent memory (a.k.a. non-volatile memory) is an emerging technology that offers fast byte-addressable durable main memory. A wealth of algorithms and libraries has been developed to explore this exciting technology. As noted by others, this has led to a significant verification gap. Towards closing this gap, we present Spirea, the first concurrent separation logic for verification of programs under a weak persistent memory model. Spirea is based on the Iris and Perennial verification frameworks, and by combining features from these logics with novel techniques it supports high-level modular reasoning about crash-safe and thread-safe programs and libraries. Spirea is fully mechanized in the Coq proof assistant and allows for interactive development of proofs with the Iris Proof Mode. We use Spirea to verify several challenging examples with modular specifications. We show how our logic can verify thread-safety and crash-safety of non-blocking durable data structures with null-recovery, in particular the Treiber stack and the Michael-Scott queue adapted to persistent memory. This is the first time durable data structures have been verified with a program logic.

APA, Harvard, Vancouver, ISO, and other styles

49

MILNE, PETER. "SUBFORMULA AND SEPARATION PROPERTIES IN NATURAL DEDUCTION VIA SMALL KRIPKE MODELS." Review of Symbolic Logic 3, no. 2 (June 2010): 175–227. http://dx.doi.org/10.1017/s175502030999030x.

Full text

Abstract:

Various natural deduction formulations of classical, minimal, intuitionist, and intermediate propositional and first-order logics are presented and investigated with respect to satisfaction of the separation and subformula properties. The technique employed is, for the most part, semantic, based on general versions of the Lindenbaum and Lindenbaum–Henkin constructions. Careful attention is paid (i) to which properties of theories result in the presence of which rules of inference, and (ii) to restrictions on the sets of formulas to which the rules may be employed, restrictions determined by the formulas occurring as premises and conclusion of the invalid inference for which a counterexample is to be constructed. We obtain an elegant formulation of classical propositional logic with the subformula property and a singularly inelegant formulation of classical first-order logic with the subformula property, the latter, unfortunately, not a product of the strategy otherwise used throughout the article. Along the way, we arrive at an optimal strengthening of the subformula results for classical first-order logic obtained as consequences of normalization theorems by Dag Prawitz and Gunnar Stålmarck.

APA, Harvard, Vancouver, ISO, and other styles

50

Mulder, Ike, Łukasz Czajka, and Robbert Krebbers. "Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic." Proceedings of the ACM on Programming Languages 7, PLDI (June 6, 2023): 1340–64. http://dx.doi.org/10.1145/3591275.

Full text

Abstract:

Concurrent separation logic has been responsible for major advances in the formal verification of fine-grained concurrent algorithms and data structures such as locks, barriers, queues, and reference counters. The key ingredient of the verification of a fine-grained program is an invariant, which relates the physical data representation (on the heap) to a logical representation (in mathematics) and to the state of the threads (using a form of ghost state). An invariant is typically represented as a disjunction of logical states, but this disjunctive nature makes invariants a difficult target for automated verification. Current approaches roughly suffer from two problems. They use backtracking to introduce disjunctions in an uninformed manner, which can lead to unprovable goals if an appropriate case analysis has not been made before choosing the disjunct. Moreover, they eliminate disjunctions too eagerly, which can cause poor efficiency. While disjunctions are no problem for automated provers based on classical (i.e., non-separating) logic, the challenges with disjunctions are prominent in the study of proof automation for intuitionistic logic. We take inspiration from that area—specifically, based on ideas from connection calculus , we design a simple multi-succedent calculus for separation logic with disjunctions featuring a novel concept of a connection . While our calculus is not complete, it has the advantage that it can be extended with features of the state-of-the-art concurrent separation logic Iris (such as modalities, higher-order quantification, ghost state, and invariants), and can be implemented effectively in the Coq proof assistant with little need for backtracking. We evaluate the practicality on 24 challenging benchmarks, 14 of which we can verify fully automatically.

APA, Harvard, Vancouver, ISO, and other styles

We offer discounts on all premium plans for authors whose works are included in thematic literature selections. Contact us to get a unique promo code!