Zobrazeno 1 - 10
of 114
pro vyhledávání: '"Wies, Thomas"'
We study the implementability problem for an expressive class of symbolic communication protocols involving multiple participants. Our symbolic protocols describe infinite states and data values using dependent refinement predicates. Implementability
Externí odkaz:
http://arxiv.org/abs/2411.05722
Autor:
Wolff, Sebastian, Gupta, Ekanshdeep, Esen, Zafer, Hojjat, Hossein, Rümmer, Philipp, Wies, Thomas
Memory safety is an essential correctness property of software systems. For programs operating on linked heap-allocated data structures, the problem of proving memory safety boils down to analyzing the possible shapes of data structures, leading to t
Externí odkaz:
http://arxiv.org/abs/2408.09037
Many temporal safety properties of higher-order programs go beyond simple event sequencing and require an automaton register (or "accumulator") to express, such as input-dependency, event summation, resource usage, ensuring equal event magnitude, com
Externí odkaz:
http://arxiv.org/abs/2408.02791
We present and verify template algorithms for lock-free concurrent search structures that cover a broad range of existing implementations based on lists and skiplists. Our linearizability proofs are fully mechanized in the concurrent separation logic
Externí odkaz:
http://arxiv.org/abs/2405.13271
Multiparty session types (MSTs) are a type-based approach to verifying communication protocols, represented as global types in the framework. We present a precise subtyping relation for asynchronous MSTs with communicating state machines (CSMs) as im
Externí odkaz:
http://arxiv.org/abs/2401.16395
Separation logic is often praised for its ability to closely mimic the locality of state updates when reasoning about them at the level of assertions. The prover only needs to concern themselves with the footprint of the computation at hand, i.e., th
Externí odkaz:
http://arxiv.org/abs/2307.15549
Multiparty session types (MSTs) are a type-based approach to verifying communication protocols. Central to MSTs is a projection operator: a partial function that maps protocols represented as global types to correct-by-construction implementations fo
Externí odkaz:
http://arxiv.org/abs/2305.17079
We present a new flow framework for separation logic reasoning about programs that manipulate general graphs. The framework overcomes problems in earlier developments: it is based on standard fixed point theory, guarantees least flows, rules out vani
Externí odkaz:
http://arxiv.org/abs/2304.04886
Publikováno v:
Proc. ACM Program. Lang. 7, PLDI, Article 182 (June 2023), 24 pages
Proving linearizability of concurrent data structures remains a key challenge for verification. We present temporal interpolation as a new proof principle to conduct such proofs using hindsight arguments within concurrent separation logic. Temporal r
Externí odkaz:
http://arxiv.org/abs/2209.13692
Publikováno v:
Proc. ACM Program. Lang. 6, OOPSLA2, Article 174 (October 2022), 30 pages
Verifying fine-grained optimistic concurrent programs remains an open problem. Modern program logics provide abstraction mechanisms and compositional reasoning principles to deal with the inherent complexity. However, their use is mostly confined to
Externí odkaz:
http://arxiv.org/abs/2207.02355