Verifying a Compiler for Java Threads

DOI10.1007/978-3-642-11957-6_23zbMath1260.68080OpenAlexW1521087854MaRDI QIDQ3558240

Andreas Lochbihler

Publication date: 4 May 2010

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-11957-6_23

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Related Items (9)

A decision procedure for (co)datatypes in SMT solvers ⋮ A Decision Procedure for (Co)datatypes in SMT Solvers ⋮ From Jinja bytecode to term rewriting: a complexity reflecting transformation ⋮ Mechanising a type-safe model of multithreaded Java with a verified compiler ⋮ A Formal Proof of the Computation of Hermite Normal Form in a General Setting ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ Compositional reasoning for shared-variable concurrent programs ⋮ An operational semantics for object-oriented concepts based on the class hierarchy ⋮ Animating the Formalised Semantics of a Java-Like Language

Uses Software

• Isabelle/HOL
• Jinja Threads
• BicolanoMT

This page was built for publication: Verifying a Compiler for Java Threads