Tool-assisted specification and verification of typed low-level languages

DOI10.1007/S10817-005-0084-6MaRDI QIDQ861687zbMATH OpenOpenAlexFDO

Authors Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa

Publication date 30 January 2007

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-005-0084-6

zbMATH Keywords

bytecode verificationJava Cardtheorem provingvirtual machine

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• Fundamental Approaches to Software Engineering
• Java bytecode verification: Algorithms and formalizations
• scientific article; zbMATH DE number 1701360
• Verified bytecode verifiers.
• scientific article; zbMATH DE number 2043539

Cites work

• A type system for JVM threads
• Abstract State Machines
• Automated theorem proving by test set induction
• External rewriting for skeptical proof assistants
• Fundamental Approaches to Software Engineering
• scientific article; zbMATH DE number 1650458 (Why is no real title available?)
• scientific article; zbMATH DE number 1692947 (Why is no real title available?)
• scientific article; zbMATH DE number 1696760 (Why is no real title available?)
• scientific article; zbMATH DE number 1701360 (Why is no real title available?)
• scientific article; zbMATH DE number 4072439 (Why is no real title available?)
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• scientific article; zbMATH DE number 1980941 (Why is no real title available?)
• scientific article; zbMATH DE number 2043539 (Why is no real title available?)
• scientific article; zbMATH DE number 1927413 (Why is no real title available?)
• scientific article; zbMATH DE number 1798185 (Why is no real title available?)
• scientific article; zbMATH DE number 2086505 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• Java bytecode verification: Algorithms and formalizations
• Language prototyping: An algebraic specification approach
• Term Rewriting and All That
• Typing a multi-language intermediate code
• Verified bytecode subroutines
• Verified bytecode verifiers.

Cited in

(4)

• Language-based program verification via expressive types
• scientific article; zbMATH DE number 2043539 (Why is no real title available?)
• Modular and automated type-soundness verification for language extensions
• Theorem Proving in Higher Order Logics

Describes a project that uses

Uses Software

• OCaml
• Coq
• LETOS
• Jakarta
• Centaur

This page was built for publication: Tool-assisted specification and verification of typed low-level languages

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