Výsledky vyhledávání - "Pedro da Rocha Pinto"

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

Zobrazit plný text záznamu

A perspective on specifying and verifying concurrent modules

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

The specification of a concurrent program module, and the verification of implementations and clients with respect to such a specification, are difficult problems. A specification should be general enough that any reasonable implementation satisfies

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::793f2e9fb6bc258451b8c12424fd2da2
http://hdl.handle.net/10044/1/58595

Zobrazit plný text záznamu

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

Zobrazit plný text záznamu

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

Zobrazit plný text záznamu

Fault-Tolerant Resource Reasoning

Autor: Gian Ntzik, Pedro da Rocha Pinto, Philippa Gardner

Publikováno v: Programming Languages and Systems ISBN: 9783319265285
APLAS
13th Asian Symposium on Programming Languages and Systems

Separation logic has been successful at verifying that programs do not crash due to illegal use of resources. The underlying assumption, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, e.g. pow

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::da7f13e761763c85c2fb35107a3a5b95
http://hdl.handle.net/10044/1/33183

Zobrazit plný text záznamu

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

Zobrazit plný text záznamu

A simple abstraction for complex concurrent indexes

Autor: Mike Dodds, Mark Wheelhouse, Philippa Gardner, Pedro da Rocha Pinto, Thomas Dinsdale-Young

Publikováno v: 2011 ACM international conference on Object oriented programming systems languages and applications
OOPSLA

Indexes are ubiquitous. Examples include associative arrays, dictionaries, maps and hashes used in applications such as databases, file systems and dynamic languages. Abstractly, a sequential index can be viewed as a partial function from keys to val

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5eb8776a8a72f23d3970a53090aad919
http://hdl.handle.net/10044/1/95171

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání