Zobrazeno 1 - 10
of 38
pro vyhledávání: '"Pedro da Rocha Pinto"'
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
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
http://hdl.handle.net/10044/1/58595
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
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
https://doi.org/10.1007/978-3-662-54434-1_16
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
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
https://pure.au.dk/portal/da/publications/modular-termination-verification-for-nonblocking-concurrency(ca933a23-3a96-42fd-a8de-4b773f279846).html
Publikováno v:
Programming Languages and Systems ISBN: 9783319265285
APLAS
13th Asian Symposium on Programming Languages and Systems
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
http://hdl.handle.net/10044/1/33183
Autor:
Oliveira Vale, Arthur1 arthur.oliveiravale@yale.edu, Shao, Zhong1 zhong.shao@yale.edu, Chen, Yixuan1 yixuan.chen@yale.edu
Publikováno v:
Journal of the ACM. Apr2024, Vol. 71 Issue 2, p1-107. 107p.
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
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
https://doi.org/10.1007/978-3-662-44202-9_9
Publikováno v:
2011 ACM international conference on Object oriented programming systems languages and applications
OOPSLA
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
http://hdl.handle.net/10044/1/95171
Autor:
PAGEL, JENS1, ZULEGER, FLORIAN1
Publikováno v:
ACM Transactions on Programming Languages & Systems. Jul2022, Vol. 44 Issue 3, p1-40. 40p.
Autor:
LORCH, JACOB R.1, YIXUAN CHEN2 yixuan.chen@yale.edu, KAPRITSOS, MANOS3, HAOJUN MA3 mahaojun@umich.edu, PARNO, BRYAN4 parno@cmu.edu, QADEER, SHAZ5 shaz.qadeer@gmail.com, SHARMA, UPAMANYU6 upamanyu@mit.edu, WILCOX, JAMES R.7 james@certora.com, XUEYUAN ZHAO4 xueyuanz@alumni.cmu.edu
Publikováno v:
ACM Transactions on Programming Languages & Systems. 2022, Vol. 44 Issue 2, p1-39. 39p.