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
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
