A verifying compiler for a multi-threaded object-oriented language

MaRDI QIDQ5447372zbMATH OpenFDO

Authors K. Rustan M. Leino, Wolfram Schulte

Publication date 6 March 2008

zbMATH Keywords

students' guide to automatic program verification

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verifying a Compiler for Java Threads
• Verifying an Open Compiler Using Multi-language Semantics
• Verifying optimizations for concurrent programs
• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 2087551

Cited in

(6)

• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Verifying Whiley programs with Boogie
• Verifying a Compiler for Java Threads
• A Machine Checked Soundness Proof for an Intermediate Verification Language
• Verifying an Open Compiler Using Multi-language Semantics
• Verification of Equivalent-Results Methods

Describes a project that uses

Uses Software

• ESC/Java
• KRAKATOA
• JML
• KeY
• SPARK
• LARCH
• SIMPLIFY
• Boogie

This page was built for publication: A verifying compiler for a multi-threaded object-oriented language

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