Zobrazeno 1 - 10
of 121
pro vyhledávání: '"Dreyer, Derek"'
Publikováno v:
Proc. ACM Program. Lang. 7, OOPSLA1, Article 93 (April 2023)
Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundations. In this paper, we argue that a single unified theory can be used
Externí odkaz:
http://arxiv.org/abs/2303.03111
Publikováno v:
Journal of the ACM; Dec2024, Vol. 71 Issue 6, p1-75, 75p
Publikováno v:
Proc. ACM Program. Lang. 6, OOPSLA2, Article 135 (October 2022), 26 pages (2022)
Hypersafety properties of arity $n$ are program properties that relate $n$ traces of a program (or, more generally, traces of $n$ programs). Classic examples include determinism, idempotence, and associativity. A number of relational program logics h
Externí odkaz:
http://arxiv.org/abs/2209.07448
Publikováno v:
Logical Methods in Computer Science, Volume 7, Issue 2 (June 7, 2011) lmcs:698
Appel and McAllester's "step-indexed" logical relations have proven to be a simple and effective technique for reasoning about programs in languages with semantically interesting types, such as general recursive types and general reference types. How
Externí odkaz:
http://arxiv.org/abs/1103.0510
Publikováno v:
Communications of the ACM; Apr2021, Vol. 64 Issue 4, p144-152, 9p, 1 Color Photograph, 8 Diagrams
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Autor:
ROSSBERG, ANDREAS1 rossberg@mpi-sws.org, DREYER, DEREK2
Publikováno v:
ACM Transactions on Programming Languages & Systems. Apr2013, Vol. 35 Issue 1, p2:1-2:84. 84p.
Publikováno v:
29th European Conference on Object-Oriented Programming
Leibniz International Proceedings in Informatics
Leibniz International Proceedings in Informatics
The field of concurrent separation logics (CSLs) has recently undergone two exciting developments: (1) the Iris framework for encoding and unifying advanced higher-order CSLs and formalizing them in Coq, and (2) the adaptation of CSLs to account for
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d6ee65e0d984451a363f96e853f02f1f
https://hdl.handle.net/21.11116/0000-0000-76DE-221.11116/0000-0008-E7B1-B
https://hdl.handle.net/21.11116/0000-0000-76DE-221.11116/0000-0008-E7B1-B
Publikováno v:
BASE-Bielefeld Academic Search Engine
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
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c67242a102fb498d314051223b447d46