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

DOI10.1007/s10817-005-0084-6zbMath1107.68027OpenAlexW2142949137MaRDI QIDQ861687

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

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

theorem provingvirtual machineJava Cardbytecode verification

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Uses Software

• Coq
• Jakarta
• LETOS
• OCaml
• Centaur

Cites Work

• Automated theorem proving by test set induction
• Java bytecode verification: Algorithms and formalizations
• Verified bytecode subroutines
• A type system for JVM threads
• External rewriting for skeptical proof assistants
• Verified bytecode verifiers.
• Language Prototyping: An Algebraic Specification Approach
• Abstract State Machines
• Term Rewriting and All That
• Typing a multi-language intermediate code
• Fundamental Approaches to Software Engineering
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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