Pages that link to "Item:Q4329634"
From MaRDI portal
The following pages link to Hoare logic for Java in Isabelle/HOL (Q4329634):
Displaying 27 items.
- An observationally complete program logic for imperative higher-order functions (Q387994) (← links)
- Verification of object-oriented programs: a transformational approach (Q439944) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- A dynamic logic for deductive verification of multi-threaded programs (Q470007) (← links)
- On theorem prover-based testing (Q470025) (← links)
- Lazy behavioral subtyping (Q710675) (← links)
- rCOS: a refinement calculus of object systems (Q854169) (← links)
- A generic complete dynamic logic for reasoning about purity and effects (Q973056) (← links)
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++ (Q1040775) (← links)
- A UTP approach for rTiMo (Q1624596) (← links)
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← links)
- Mechanising a type-safe model of multithreaded Java with a verified compiler (Q1663233) (← links)
- An assertion-based proof system for multithreaded Java (Q1770359) (← links)
- Verified bytecode verification and type-certifying compilation (Q1881665) (← links)
- Semantics, calculi, and analysis for object-oriented specifications (Q2390933) (← links)
- A program logic for resources (Q2463560) (← links)
- A proof outline logic for object-oriented programming (Q2571207) (← links)
- Specification and verification challenges for sequential object-oriented programs (Q2643131) (← links)
- \(\mu\)Java: Embedding a programming language in a theorem prover (Q2752051) (← links)
- (Q2764133) (← links)
- Ensuring the correctness of lightweight tactics for JavaCard dynamic logic (Q2871841) (← links)
- Equational Theories of Abnormal Termination Based on Kleene Algebra (Q2988362) (← links)
- Computing Preconditions and Postconditions of While Loops (Q3105751) (← links)
- Reasoning About Resources in the Embedded Systems Language Hume (Q3460507) (← links)
- Formal Methods for Components and Objects (Q5311301) (← links)
- Formal Methods for Open Object-Based Distributed Systems (Q5902541) (← links)
- Integrating ADTs in KeY and their application to history-based reasoning about collection (Q6185826) (← links)
