Pages that link to "Item:Q1881670"

The following pages link to The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML (Q1881670):

Displaying 21 items.

• JCML: A specification language for the runtime verification of Java card programs (Q436381) (← links)
• Verification conditions for source-level imperative programs (Q465685) (← links)
• A dynamic logic for deductive verification of multi-threaded programs (Q470007) (← links)
• Synthesis of ML programs in the system Coq (Q1322847) (← links)
• Weakest pre-condition reasoning for Java programs with JML annotations (Q1881666) (← links)
• Deductive verification of floating-point Java programs in KeY (Q2233510) (← links)
• A program logic for resources (Q2463560) (← links)
• A proof outline logic for object-oriented programming (Q2571207) (← links)
• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts (Q2642466) (← links)
• Are the logical foundations of verifying compiler prototypes matching user expectations? (Q2643125) (← links)
• Specification and verification challenges for sequential object-oriented programs (Q2643131) (← links)
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach (Q2802468) (← links)
• Secure information flow by self-composition (Q3103613) (← links)
• An Introduction to Certificate Translation (Q3184785) (← links)
• Reasoning About Resources in the Embedded Systems Language Hume (Q3460507) (← links)
• Could We Have Chosen a Better Loop Invariant or Method Contract? (Q3637252) (← links)
• (Q5028422) (← links)
• (Q5094146) (← links)
• Specification and Runtime Verification of Java Card Programs (Q5179352) (← links)
• Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes (Q5452615) (← links)
• Verification of Java Programs with Generics (Q5505432) (← links)