Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 25:1-25:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{loow_et_al:LIPIcs.ECOOP.2024.25, author = {L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Cronj\"{a}ger, Caroline and Maksimovi\'{c}, Petar and Gardner, Philippa}, title = {{Compositional Symbolic Execution for Correctness and Incorrectness Reasoning}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {25:1--25:28}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-341-6}, ISSN = {1868-8969}, year = {2024}, volume = {313}, editor = {Aldrich, Jonathan 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.2024.25}, URN = {urn:nbn:de:0030-drops-208741}, doi = {10.4230/LIPIcs.ECOOP.2024.25}, annote = {Keywords: separation logic, incorrectness logic, symbolic execution, bi-abduction} }
Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimović, and Philippa Gardner. Matching Plans for Frame Inference in Compositional Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{loow_et_al:LIPIcs.ECOOP.2024.26, author = {L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Maksimovi\'{c}, Petar and Gardner, Philippa}, title = {{Matching Plans for Frame Inference in Compositional Reasoning}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {26:1--26:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-341-6}, ISSN = {1868-8969}, year = {2024}, volume = {313}, editor = {Aldrich, Jonathan 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.2024.26}, URN = {urn:nbn:de:0030-drops-208751}, doi = {10.4230/LIPIcs.ECOOP.2024.26}, annote = {Keywords: Compositional reasoning, separation logic, frame inference} }
Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Nat Karmios, Petar Maksimović, and Philippa Gardner. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 13:1-13:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@Article{loow_et_al:DARTS.10.2.13, author = {L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Cronj\"{a}ger, Caroline and Karmios, Nat and Maksimovi\'{c}, Petar and Gardner, Philippa}, title = {{Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact)}}, pages = {13:1--13:2}, journal = {Dagstuhl Artifacts Series}, ISBN = {978-3-95977-342-3}, ISSN = {2509-8195}, year = {2024}, volume = {10}, number = {2}, editor = {L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Cronj\"{a}ger, Caroline and Karmios, Nat 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.10.2.13}, URN = {urn:nbn:de:0030-drops-209110}, doi = {10.4230/DARTS.10.2.13}, annote = {Keywords: separation logic, incorrectness logic, symbolic execution, bi-abduction} }
Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)
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)
@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} }
Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)
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)
@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} }
Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)
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)
@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} }
Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)
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)
@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} }
Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)
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)
@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} }
Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)
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)
@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} }
Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)
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)
@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} }
Published in: Dagstuhl Reports, Volume 5, Issue 5 (2016)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)
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)
@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} }
Feedback for Dagstuhl Publishing