Theorems for free from separation logic specifications

Autor: Guilhem Jaber, Nikos Tzevelekos, Thomas Dinsdale-Young, Kasper Svendsen, Armaël Guéneau, Lars Birkedal

Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (ICFP), pp.1-29. ⟨10.1145/3473586⟩
Birkedal, L, Dinsdale-Young, T, Guéneau, A, Jaber, G, Svendsen, K & Tzevelekos, N 2021, ' Theorems for free from separation logic specifications ', Proceedings of the ACM on Programming Languages, vol. 5, no. ICFP, 81 . https://doi.org/10.1145/3473586
Proceedings of the ACM on Programming Languages, 2021, 5 (ICFP), pp.1-29. ⟨10.1145/3473586⟩

International audience; 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 intuit

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e35f5012f890d1efb00d735a96ce54c2
https://hal.archives-ouvertes.fr/hal-03510684

Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)

Autor: Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner

Publikováno v: MFPS

The specification of a concurrent program module is a difficult problem. The specifications must be strong enough to enable reasoning about the intended clients without reference to the underlying module implementation. We survey a range of verificat

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::17813f4e5ddd85aabdff9a8fa522cd3f

Caper

Autor: Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, Lars Birkedal

Publikováno v: Programming Languages and Systems ISBN: 9783662544334
26th European Symposium on Programming, ESOP 2017
Dinsdale-Young, T, da Rocha Pinto, P, Andersen, K J A & Birkedal, L 2017, Caper : Automatic Verification for Fine-Grained Concurrency . in H Yang (ed.), Programming Languages and Systems : 26th European Symposium on Programming, ESOP 2017 . vol. 10201, Springer VS, Berlin, Heidelberg, Lecture Notes in Computer Science, vol. 10201, pp. 420-447, European Symposium on Programming, Uppsala, Sweden, 22/04/2017 . https://doi.org/10.1007/978-3-662-54434-1_16

Recent program logics based on separation logic emphasise a modular approach to proving functional correctness for fine-grained concurrent programs. However, these logics have no automation support. In this paper, we present Caper, a prototype tool f

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::bb2737d0399b815f5a4af5318b2ad907
https://doi.org/10.1007/978-3-662-54434-1_16

Modular termination verification for non-blocking concurrency

Autor: Pedro da Rocha Pinto, Philippa Gardner, Julian Sutherland, Thomas Dinsdale-Young

Publikováno v: Da Rocha Pinto, P, Dinsdale-Young, T, Gardner, P & Sutherland, J 2016, Modular termination verification for non-blocking concurrency . in P Thiemann (ed.), Programming Languages and Systems-25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings . vol. 9632, Springer, Lecture Notes in Computer Science (LNCS), vol. 9632, pp. 176-201, 25th European Symposium on Programming, ESOP 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, Netherlands, 02/04/2016 . https://doi.org/10.1007/978-3-662-49498-1_8
Programming Languages and Systems ISBN: 9783662494974
ESOP
25th European Symposium on Programming, ESOP 2016

© Springer-Verlag Berlin Heidelberg 2016.We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::724f43a2e369ff0b37ded333dbed9f93
https://pure.au.dk/portal/da/publications/modular-termination-verification-for-nonblocking-concurrency(ca933a23-3a96-42fd-a8de-4b773f279846).html

TaDA: A Logic for Time and Data Abstraction

Autor: Pedro da Rocha Pinto, Philippa Gardner, Thomas Dinsdale-Young

Publikováno v: ECOOP 2014 – Object-Oriented Programming ISBN: 9783662442012
ECOOP
Da Rocha Pinto, P, Dinsdale-Young, T & Gardner, P 2014, TaDA : A logic for time and data abstraction . in R Jones (ed.), ECOOP 2014 – Object-Oriented Programming : 28th European Conference, Uppsala, Sweden, July 28 – August 1, 2014. Proceedings . Springer, Lecture Notes in Computer Science, vol. 8586, pp. 207-231, European Conference on Object-Oriented Programming, Uppsala, Sweden, 28/07/2014 . https://doi.org/10.1007/978-3-662-44202-9_9
European Conference on Object-Oriented Programming, ECOOP 2014

To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well-known correctness

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::191339166a206348ab873becbdf5ea3f
https://doi.org/10.1007/978-3-662-44202-9_9