A Basis for Verifying Multi-threaded Programs
From MaRDI portal
Publication:3617715
DOI10.1007/978-3-642-00590-9_27zbMath1234.68078OpenAlexW1555179958MaRDI QIDQ3617715
K. Rustan M. Leino, Peter Müller
Publication date: 31 March 2009
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-00590-9_27
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (14)
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers ⋮ A First-Order Logic with Frames ⋮ Automatic Inference of Access Permissions ⋮ Product programs in the wild: retrofitting program verifiers to check information flow security ⋮ Ghost signals: verifying termination of busy waiting ⋮ Effect-polymorphic behaviour inference for deadlock checking ⋮ Stepwise refinement of heap-manipulating code in Chalice ⋮ Temporary Read-Only Permissions for Separation Logic ⋮ The Relationship between Separation Logic and Implicit Dynamic Frames ⋮ Enforcing Structural Invariants Using Dynamic Frames ⋮ The dynamic frames theory ⋮ Unnamed Item ⋮ Unifying separation logic and region logic to allow interoperability ⋮ On the relation between concurrent separation logic and concurrent Kleene algebra
Uses Software
This page was built for publication: A Basis for Verifying Multi-threaded Programs
