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) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

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)

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

Describes a project that uses

Uses Software

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

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)