2 papers
cs.LO2026
Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)
Ömer Şakar, Soham Chakraborty, Marieke Huisman +1
Concurrent programming under weak memory concurrency faces substantial challenges to ensure correctness due to program behaviors that cannot be explained by thread interleaving, a.…
cs.LO2026
Predicate Subtypes in VerCors
Tycho Dubbeling, Marieke Huisman, Ömer Şakar
Predicate subtypes provide an attractive mechanism to specify range constraints on variable declarations. This paper discusses how we add support for predicate subtypes to the VerC…