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

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

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)

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

Describes a project that uses

Uses Software

• Smallfoot
• Boogie
• VeriFast
• z3

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)