scientific article; zbMATH DE number 2043539

MaRDI QIDQ4447243zbMATH OpenFDO

Authors Gilles Barthe, Sorin Stratulat

Publication date 16 February 2004

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2706/27060337.htm

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theory of software (68N99)

Recommendations

• scientific article; zbMATH DE number 1692947
• Tool-assisted specification and verification of typed low-level languages
• Fundamental Approaches to Software Engineering
• Java bytecode verification: Algorithms and formalizations
• scientific article; zbMATH DE number 1857507

Cited in

(9)

• A B model for ensuring soundness of a large subset of the Java card virtual machine
• scientific article; zbMATH DE number 1629941 (Why is no real title available?)
• Tool-assisted specification and verification of typed low-level languages
• Automated Certification of Implicit Induction Proofs
• Correctness of Java card method lookup via logical relations
• Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
• scientific article; zbMATH DE number 1692947 (Why is no real title available?)
• scientific article; zbMATH DE number 2086505 (Why is no real title available?)
• Mechanically certifying formula-based Noetherian induction reasoning

Describes a project that uses

Uses Software

• Coq
• Jakarta
• SPIKE

This page was built for publication:

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