A Basis for Verifying Multi-threaded Programs

DOI10.1007/978-3-642-00590-9_27MaRDI QIDQ3617715zbMATH OpenOpenAlexFDO

Authors 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

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 2087551
• Modular verification of multithreaded programs
• A shared-variable concurrency analysis of multi-threaded object-oriented programs
• scientific article; zbMATH DE number 2087419
• scientific article; zbMATH DE number 1903353

Cited in

(20)

• Unifying separation logic and region logic to allow interoperability
• Stepwise refinement of heap-manipulating code in Chalice
• On the relation between concurrent separation logic and concurrent Kleene algebra
• scientific article; zbMATH DE number 1701757 (Why is no real title available?)
• Automatic inference of access permissions
• Temporary read-only permissions for separation logic
• The relationship between separation logic and implicit dynamic frames
• Enforcing structural invariants using dynamic frames
• Effect-polymorphic behaviour inference for deadlock checking
• Checking a Multithreaded Algorithm with  + CAL
• Verifying a Compiler for Java Threads
• scientific article; zbMATH DE number 2087551 (Why is no real title available?)
• Concise read-only specifications for better synthesis of programs with pointers
• A first-order logic with frames
• Concurrent Robin Hood hashing
• The dynamic frames theory
• Derivable partial locking for algebraic data types
• Modular verification of multithreaded programs
• Product programs in the wild: retrofitting program verifiers to check information flow security
• Ghost signals: verifying termination of busy waiting

Describes a project that uses

Uses Software

• z3
• VeriFast
• Boogie
• Smallfoot

This page was built for publication: A Basis for Verifying Multi-threaded Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3617715)