DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2023.19

Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding

Authors: Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract

Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised, but established results and errors need not be reachable. OX function specifications are thus incompatible with true bug-finding supported by symbolic execution tools such as Pulse and Pulse-X. In contrast, under-approximating (UX) program logics, such as incorrectness separation logic, are used to find true results and bugs: established results and errors are reachable, but there is no mechanism for understanding if all terminating behaviour has been characterised. We introduce exact separation logic (ESL), which provides fully-verified function specifications compatible with both OX verification and UX true bug-funding: all terminating behaviour is characterised and all established results and errors are reachable. We prove soundness for ESL with mutually recursive functions, demonstrating, for the first time, function compositionality for a UX logic. We show that UX program logics require subtle definitions of internal and external function specifications compared with the familiar definitions of OX logics. We investigate the expressivity of ESL and, for the first time, explore the role of abstraction in UX reasoning by verifying abstract ESL specifications of various data-structure algorithms. In doing so, we highlight the difference between abstraction (hiding information) and over-approximation (losing information). Our findings demonstrate that abstraction cannot be used as freely in UX logics as in OX logics, but also that it should be feasible to use ESL to provide tractable function specifications for self-contained, critical code, which would then be used for both verification and true bug-finding.

Cite as

Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner. Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 19:1-19:27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{maksimovic_et_al:LIPIcs.ECOOP.2023.19,
  author =	{Maksimovi\'{c}, Petar and Cronj\"{a}ger, Caroline and L\"{o}\"{o}w, Andreas and Sutherland, Julian and Gardner, Philippa},
  title =	{{Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{19:1--19:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.19},
  URN =		{urn:nbn:de:0030-drops-182123},
  doi =		{10.4230/LIPIcs.ECOOP.2023.19},
  annote =	{Keywords: Separation logic, program correctness, program incorrectness, abstraction}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2023.28

Concurrent Realizability on Conjunctive Structures

Authors: Emmanuel Beffara, Félix Castro, Mauricio Guillermo, and Étienne Miquey

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract

This work aims at exploring the algebraic structure of concurrent processes and their behavior independently of a particular formalism used to define them. We propose a new algebraic structure called conjunctive involutive monoidal algebra (CIMA) as a basis for an algebraic presentation of concurrent realizability, following ideas of the algebrization program already developed in the realm of classical and intuitionistic realizability. In particular, we show how any CIMA provides a sound interpretation of multiplicative linear logic. This new structure involves, in addition to the tensor and the orthogonal map, a parallel composition. We define a reference model of this structure as induced by a standard process calculus and we use this model to prove that parallel composition cannot be defined from the conjunctive structure alone.

Cite as

Emmanuel Beffara, Félix Castro, Mauricio Guillermo, and Étienne Miquey. Concurrent Realizability on Conjunctive Structures. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 28:1-28:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{beffara_et_al:LIPIcs.FSCD.2023.28,
  author =	{Beffara, Emmanuel and Castro, F\'{e}lix and Guillermo, Mauricio and Miquey, \'{E}tienne},
  title =	{{Concurrent Realizability on Conjunctive Structures}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{28:1--28:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.28},
  URN =		{urn:nbn:de:0030-drops-180124},
  doi =		{10.4230/LIPIcs.FSCD.2023.28},
  annote =	{Keywords: Realizability, Process Algebras, Concurrent Processes, Linear Logic}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.CONCUR.2022.2

Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions (Invited Talk)

Authors: Philippa Gardner

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract

Scalable verification for concurrent programs with shared memory is a long-standing, difficult problem. In 2004, O'Hearn and Brookes introduced concurrent separation logic to provide compositional reasoning about coarse-grained concurrent programs with synchronisation primitives (Gödel prize, 2016). In 2010, I introduced logical abstraction (the fiction of separation) to CSL, developing the CAP logic for reasoning about fine-grained concurrent programs in general and fine-grained lock algorithms in particular. In one logic, it was possible to provide two-sided specifications of concurrent operations, with formally verified implementations and clients. In 2014, I introduced logical atomicity (the fiction of atomicity) to concurrent separation logics, developing the TaDA logic to capture when individual operations behave atomically. Unlike CAP, where synchronisation primitives leak into the specifications, with TaDA the specifications are "just right" in that they provide more general atomic functions specifications to capture, for example, the full behaviour of lock operations. In 2021, I introduced environment liveness conditions to concurrent separation logics, developing the TaDA Live logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking: that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. The fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment. In this talk, I will explain this on-going journey in the wonderful world of concurrent separation logics. I will also explain why I have a bright green office chair in the corner of my office, patterned in gold lamé. Many thanks to my fabulous coauthors on concurrent separation logics: Thomas Dinsdale-Young, Emanuele D'Osualdo, Mike Dodds, Azadeh Farzan, Matthew Parkinson, Pedro da Rocha Pinto, Julian Sutherland, Viktor Vafeiadis and more. Suggested Reading: - Peter O'Hearn: Resources, Concurrency and Local Reasoning, Journal of Theoretical Computer Science, Festschrift for John C Reynolds 70th birthday, 2007. - Thomas Dinsdale-Young, Pedro da Rocha Pinto and Philippa Gardner: A Perspective on Specifying and Verifying Concurrent Modules, Journal of Logical and Algebraic Methods in Programming, 2018. - Emanuele D'Osualdo, Azadeh Farzan, Philippa Gardner and Julian Sutherland: TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), 2021.

Cite as

Philippa Gardner. Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions (Invited Talk). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, p. 2:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gardner:LIPIcs.CONCUR.2022.2,
  author =	{Gardner, Philippa},
  title =	{{Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.2},
  URN =		{urn:nbn:de:0030-drops-170659},
  doi =		{10.4230/LIPIcs.CONCUR.2022.2},
  annote =	{Keywords: Concurrent separation logic}
}

Document

Artifact

DOI: 10.4230/DARTS.6.2.5

A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact)

Authors: Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, and Philippa Gardner

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract

This artifact contains the implementation of JaVerT.Click, a symbolic analysis tool for modern event-driven Web applications. The tool extends JaVerT 2.0, a state-of-the-art symbolic execution tool for JavaScript (JS), with JS reference implementations of the DOM Core Level 1, DOM UI Events, JavaScript Promises and the JavaScript async/await APIs, all underpinned by a simple Core Event Semantics which is sufficiently expressive to describe the event models underlying these APIs. Our reference implementations mostly follow the respective standards line-by-line and are all thoroughly tested against the official test suite. We also evaluate JaVerT.Click by performing symbolic analysis on two real-world libraries: cash and p-map, finding three previously unknown bugs.

Cite as

Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, and Philippa Gardner. A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 5:1-5:3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{sampaio_et_al:DARTS.6.2.5,
  author =	{Sampaio, Gabriela and Fragoso Santos, Jos\'{e} and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact)}},
  pages =	{5:1--5:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Sampaio, Gabriela and Fragoso Santos, Jos\'{e} and Maksimovi\'{c}, Petar and Gardner, Philippa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.5},
  URN =		{urn:nbn:de:0030-drops-132028},
  doi =		{10.4230/DARTS.6.2.5},
  annote =	{Keywords: Events, DOM, JavaScript, promises, symbolic execution, bug-finding}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2020.21

Data Consistency in Transactional Storage Systems: A Centralised Semantics

Authors: Shale Xiong, Andrea Cerone, Azalea Raad, and Philippa Gardner

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract

We introduce an interleaving operational semantics for describing the client-observable behaviour of atomic transactions on distributed key-value stores. Our semantics builds on abstract states comprising centralised, global key-value stores and partial client views. Using our abstract states, we present operational definitions of well-known consistency models in the literature, and prove them to be equivalent to their existing declarative definitions using abstract executions. We explore two applications of our operational framework: 1) verifying that the COPS replicated database and the Clock-SI partitioned database satisfy their consistency models using trace refinement, and 2) proving invariant properties of client programs.

Cite as

Shale Xiong, Andrea Cerone, Azalea Raad, and Philippa Gardner. Data Consistency in Transactional Storage Systems: A Centralised Semantics. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 21:1-21:31, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{xiong_et_al:LIPIcs.ECOOP.2020.21,
  author =	{Xiong, Shale and Cerone, Andrea and Raad, Azalea and Gardner, Philippa},
  title =	{{Data Consistency in Transactional Storage Systems: A Centralised Semantics}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{21:1--21:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.21},
  URN =		{urn:nbn:de:0030-drops-131782},
  doi =		{10.4230/LIPIcs.ECOOP.2020.21},
  annote =	{Keywords: Operational Semantics, Consistency Models, Transactions, Distributed Key-value Stores}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2020.28

A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications

Authors: Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, and Philippa Gardner

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract

We introduce a trusted infrastructure for the symbolic analysis of modern event-driven Web applications. This infrastructure consists of reference implementations of the DOM Core Level 1, DOM UI Events, JavaScript Promises and the JavaScript async/await APIs, all underpinned by a simple Core Event Semantics which is sufficiently expressive to describe the event models underlying these APIs. Our reference implementations are trustworthy in that three follow the appropriate standards line-by-line and all are thoroughly tested against the official test-suites, passing all the applicable tests. Using the Core Event Semantics and the reference implementations, we develop JaVerT.Click, a symbolic execution tool for JavaScript that, for the first time, supports reasoning about JavaScript programs that use multiple event-related APIs. We demonstrate the viability of JaVerT.Click by proving both the presence and absence of bugs in real-world JavaScript code.

Cite as

Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, and Philippa Gardner. A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 28:1-28:29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{sampaio_et_al:LIPIcs.ECOOP.2020.28,
  author =	{Sampaio, Gabriela and Fragoso Santos, Jos\'{e} and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{28:1--28:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.28},
  URN =		{urn:nbn:de:0030-drops-131853},
  doi =		{10.4230/LIPIcs.ECOOP.2020.28},
  annote =	{Keywords: Events, DOM, JavaScript, promises, symbolic execution, bug-finding}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2019.9

A Program Logic for First-Order Encapsulated WebAssembly

Authors: Conrad Watt, Petar Maksimović, Neelakantan R. Krishnaswami, and Philippa Gardner

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract

We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. We design a novel assertion syntax, tailored to WebAssembly’s stack-based semantics and the strong guarantees given by WebAssembly’s type system, and show how to adapt the standard separation logic triple and proof rules in a principled way to capture WebAssembly’s uncommon structured control flow. Using Wasm Logic, we specify and verify a simple WebAssembly B-tree library, giving abstract specifications independent of the underlying implementation. We mechanise Wasm Logic and its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formalise and fully mechanise a novel, big-step semantics of WebAssembly, which we prove equivalent, up to transitive closure, to the original WebAssembly small-step semantics. Wasm Logic is the first program logic for WebAssembly, and represents a first step towards the creation of static analysis tools for WebAssembly.

Cite as

Conrad Watt, Petar Maksimović, Neelakantan R. Krishnaswami, and Philippa Gardner. A Program Logic for First-Order Encapsulated WebAssembly. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 9:1-9:30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{watt_et_al:LIPIcs.ECOOP.2019.9,
  author =	{Watt, Conrad and Maksimovi\'{c}, Petar and Krishnaswami, Neelakantan R. and Gardner, Philippa},
  title =	{{A Program Logic for First-Order Encapsulated WebAssembly}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{9:1--9:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.9},
  URN =		{urn:nbn:de:0030-drops-108011},
  doi =		{10.4230/LIPIcs.ECOOP.2019.9},
  annote =	{Keywords: WebAssembly, program logic, separation logic, soundness, mechanisation}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2018.4

A Concurrent Specification of POSIX File Systems

Authors: Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, and Philippa Gardner

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract

POSIX is a standard for operating systems, with a substantial part devoted to specifying file-system operations. File-system operations exhibit complex concurrent behaviour, comprising multiple actions affecting different parts of the state: typically, multiple atomic reads followed by an atomic update. However, the standard's description of concurrent behaviour is unsatisfactory: it is fragmented; contains ambiguities; and is generally under-specified. We provide a formal concurrent specification of POSIX file systems and demonstrate scalable reasoning for clients. Our specification is based on a concurrent specification language, which uses a modern concurrent separation logic for reasoning about abstract atomic operations, and an associated refinement calculus. Our reasoning about clients highlights an important difference between reasoning about modules built over a heap, where the interference on the shared state is restricted to the operations of the module, and modules built over a file system, where the interference cannot be restricted as the file system is a public namespace. We introduce specifications conditional on context invariants used to restrict the interference, and apply our reasoning to the example of lock files.

Cite as

Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, and Philippa Gardner. A Concurrent Specification of POSIX File Systems. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 4:1-4:28, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ntzik_et_al:LIPIcs.ECOOP.2018.4,
  author =	{Ntzik, Gian and da Rocha Pinto, Pedro and Sutherland, Julian and Gardner, Philippa},
  title =	{{A Concurrent Specification of POSIX File Systems}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{4:1--4:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.4},
  URN =		{urn:nbn:de:0030-drops-92092},
  doi =		{10.4230/LIPIcs.ECOOP.2018.4},
  annote =	{Keywords: POSIX, concurrency, file systems, refinement, separation logic, atomicity}
}

Document

DOI: 10.4230/DagRep.5.5.1

Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191)

Authors: Lars Birkedal, Derek Dreyer, Philippa Gardner, and Zhong Shao

Published in: Dagstuhl Reports, Volume 5, Issue 5 (2016)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 15191 "Compositional Verification Methods for Next-Generation Concurrency". The seminar was successful and facilitated a stimulating interchange between the theory and practice of concurrent programming, and thereby laid the ground for the development of compositional verification methods that can scale to handle the realities of next-generation concurrency.

Cite as

Lars Birkedal, Derek Dreyer, Philippa Gardner, and Zhong Shao. Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191). In Dagstuhl Reports, Volume 5, Issue 5, pp. 1-23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{birkedal_et_al:DagRep.5.5.1,
  author =	{Birkedal, Lars and Dreyer, Derek and Gardner, Philippa and Shao, Zhong},
  title =	{{Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191)}},
  pages =	{1--23},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{5},
  editor =	{Birkedal, Lars and Dreyer, Derek and Gardner, Philippa and Shao, Zhong},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.5.1},
  URN =		{urn:nbn:de:0030-drops-53565},
  doi =		{10.4230/DagRep.5.5.1},
  annote =	{Keywords: Verification of Concurrent Programs (Models, Logics, Automated Analysis), Concurrent Programming}
}

Document

DOI: 10.4230/DagSemProc.04241.1

04241 Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems

Authors: Barbara König, Ugo Montanari, and Philippa Gardner

Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)

Abstract

Recently there has been a lot of research, combining concepts of process algebra with those of the theory of graph grammars and graph transformation systems. Both can be viewed as general frameworks in which one can specify and reason about concurrent and distributed systems. There are many areas where both theories overlap and this reaches much further than just using graphs to give a graphic representation to processes. Processes in a communication network can be seen in two different ways: as terms in an algebraic theory, emphasizing their behaviour and their interaction with the environment, and as nodes (or edges) in a graph, emphasizing their topology and their connectedness. Especially topology, mobility and dynamic reconfigurations at runtime can be modelled in a very intuitive way using graph transformation. On the other hand the definition and proof of behavioural equivalences is often easier in the process algebra setting. Also standard techniques of algebraic semantics for universal constructions, refinement and compositionality can take better advantage of the process algebra representation. An important example where the combined theory is more convenient than both alternatives is for defining the concurrent (noninterleaving), abstract semantics of distributed systems. Here graph transformations lack abstraction and process algebras lack expressiveness. Another important example is the work on bigraphical reactive systems with the aim of deriving a labelled transitions system from an unlabelled reactive system such that the resulting bisimilarity is a congruence. Here, graphs seem to be a convenient framework, in which this theory can be stated and developed. So, although it is the central aim of both frameworks to model and reason about concurrent systems, the semantics of processes can have a very different flavour in these theories. Research in this area aims at combining the advantages of both frameworks and translating concepts of one theory into the other. The Dagsuthl Seminar, which took place from 06.06. to 11.06.2004, was aimed at bringing together researchers of the two communities in order to share their ideas and develop new concepts. These proceedings4 of the do not only contain abstracts of the talks given at the seminar, but also summaries of topics of central interest. We would like to thank all participants of the seminar for coming and sharing their ideas and everybody who has contributed to the proceedings.

Cite as

Barbara König, Ugo Montanari, and Philippa Gardner. 04241 Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. In Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. Dagstuhl Seminar Proceedings, Volume 4241, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{konig_et_al:DagSemProc.04241.1,
  author =	{K\"{o}nig, Barbara and Montanari, Ugo and Gardner, Philippa},
  title =	{{04241 Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems}},
  booktitle =	{Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4241},
  editor =	{Barbara K\"{o}nig and Ugo Montanari and Philippa Gardner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04241.1},
  URN =		{urn:nbn:de:0030-drops-279},
  doi =		{10.4230/DagSemProc.04241.1},
  annote =	{Keywords: graph transformation , process calculi}
}

Document

DOI: 10.4230/DagSemProc.04241.2

Summary 1: Adhesivity, Bigraphs and Bisimulation Congruences

Authors: Pawel Sobocinski

Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)

Abstract

This paper is intended as a short informal summary of some of the topics which arose at the Dagstuhl meeting held 6/06/04-11/06/04. In particular, we shall summarise some of the content of talks by H. Ehrig, F. Gadducci, O. H. Jensen, R. Milner, B. KÃ?Â¶nig, V. Sassone and the author. The general areas include adhesive categories and generalisations, contextual labelled transition semantics for graph transformation systems via borrowed-contexts and GIPOs, and bigraphs. We shall conclude with a summary of some of the discussions which followed the aforementioned presentations.

Cite as

Pawel Sobocinski. Summary 1: Adhesivity, Bigraphs and Bisimulation Congruences. In Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. Dagstuhl Seminar Proceedings, Volume 4241, pp. 1-12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{sobocinski:DagSemProc.04241.2,
  author =	{Sobocinski, Pawel},
  title =	{{Summary 1: Adhesivity, Bigraphs and Bisimulation Congruences}},
  booktitle =	{Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4241},
  editor =	{Barbara K\"{o}nig and Ugo Montanari and Philippa Gardner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04241.2},
  URN =		{urn:nbn:de:0030-drops-286},
  doi =		{10.4230/DagSemProc.04241.2},
  annote =	{Keywords: graph transformation , category theory , bisimulation}
}

Document

DOI: 10.4230/DagSemProc.04241.3

Summary 2: Graph Grammar Verification through Abstraction

Authors: Paolo Baldan, Barbara König, and Arend Rensink

Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)

Abstract

Until now there have been few contributions concerning the verification of graph grammars, specifically of infinite-state graph grammars. This paper compares two existing approaches, based on abstractions of graph transformation systems. While in the unfolding approach graph grammars are approximated by Petri nets, in the partitioning approach graphs are abstracted according to their local structure. We describe differences and similarities of the two approaches and explain the underlying ideas.

Cite as

Paolo Baldan, Barbara König, and Arend Rensink. Summary 2: Graph Grammar Verification through Abstraction. In Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. Dagstuhl Seminar Proceedings, Volume 4241, pp. 1-9, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:DagSemProc.04241.3,
  author =	{Baldan, Paolo and K\"{o}nig, Barbara and Rensink, Arend},
  title =	{{Summary 2: Graph Grammar Verification through Abstraction}},
  booktitle =	{Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4241},
  editor =	{Barbara K\"{o}nig and Ugo Montanari and Philippa Gardner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04241.3},
  URN =		{urn:nbn:de:0030-drops-291},
  doi =		{10.4230/DagSemProc.04241.3},
  annote =	{Keywords: graph transformation , verification}
}

Document

DOI: 10.4230/DagSemProc.04241.4

Summary 3: On Graph(ic) Encodings

Authors: Roberto Bruni and Ivan Lanese

Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)

Abstract

This paper is an informal summary of different encoding techniques from process calculi and distributed formalisms to graphic frameworks. The survey includes the use of solo diagrams, term graphs, synchronized hyperedge replacement systems, bigraphs, tile models and interactive systems, all presented at the Dagstuhl Seminar 04241. The common theme of all techniques recalled here is having a graphic presentation that, at the same time, gives both an intuitive visual rendering (of processes, states, etc.) and a rigorous mathematical framework.

Cite as

Roberto Bruni and Ivan Lanese. Summary 3: On Graph(ic) Encodings. In Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. Dagstuhl Seminar Proceedings, Volume 4241, pp. 1-15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{bruni_et_al:DagSemProc.04241.4,
  author =	{Bruni, Roberto and Lanese, Ivan},
  title =	{{Summary 3: On Graph(ic) Encodings}},
  booktitle =	{Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4241},
  editor =	{Barbara K\"{o}nig and Ugo Montanari and Philippa Gardner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04241.4},
  URN =		{urn:nbn:de:0030-drops-303},
  doi =		{10.4230/DagSemProc.04241.4},
  annote =	{Keywords: graph transformation , process calculi , encodings}
}

13 Search Results for "Gardner, Philippa"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message