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

zbMATH Open1153.68016MaRDI QIDQ5447372FDOQ5447372

Authors: K. Rustan M. Leino, Wolfram Schulte 

Publication date: 6 March 2008

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

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)

Cited In (6)

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

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)