The following pages link to KeY (Q21946):
Displaying 50 items.
- Verification conditions for source-level imperative programs (Q465685) (← links)
- A logic for secure memory access of abstract state machines (Q555787) (← links)
- Mechanical inference of invariants for FOR-loops (Q604381) (← links)
- Invariant-driven specifications in Maude (Q838161) (← links)
- A comparison of tools for teaching formal software verification (Q1019026) (← links)
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++ (Q1040775) (← links)
- Verifying OpenJDK's sort method for generic collections (Q1725846) (← links)
- Understanding parameters of deductive verification: an empirical investigation of KeY (Q1791175) (← links)
- Assertion-based slicing and slice graphs (Q1941855) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- Gray-box monitoring of hyperproperties with an application to privacy (Q2147690) (← links)
- Formal specification and verification of JDK's identity hash map implementation (Q2165501) (← links)
- Deductive verification of floating-point Java programs in KeY (Q2233510) (← links)
- Uniform substitution at one Fell swoop (Q2305431) (← links)
- A verification-driven framework for iterative design of controllers (Q2335947) (← links)
- Proof pearl: The KeY to correct and stable sorting (Q2351413) (← links)
- Semantics, calculi, and analysis for object-oriented specifications (Q2390933) (← links)
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools (Q2402555) (← links)
- Refinement and retrenchment for programming language data types (Q2432217) (← links)
- A program logic for resources (Q2463560) (← links)
- Modular invariants for layered object structures (Q2507783) (← links)
- Are the logical foundations of verifying compiler prototypes matching user expectations? (Q2643125) (← links)
- Invariants Synthesis over a Combined Domain for Automated Program Verification (Q2842643) (← links)
- A Universal Machine for Biform Theory Graphs (Q2843007) (← links)
- Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic (Q2871841) (← links)
- A Proof Assistant for Alloy Specifications (Q2894289) (← links)
- (Q3021903) (← links)
- KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (Q3454120) (← links)
- Reasoning About Loops Using Vampire in KeY (Q3460073) (← links)
- Simplify: a theorem prover for program checking (Q3546294) (← links)
- Could We Have Chosen a Better Loop Invariant or Method Contract? (Q3637252) (← links)
- Principled Software Development (Q4558903) (← links)
- Fundamental Approaches to Software Engineering (Q5316441) (← links)
- Second-Order Principles in Specification Languages for Object-Oriented Programs (Q5387837) (← links)
- Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics (Q5387854) (← links)
- Automating Verification of Loops by Parallelization (Q5387902) (← links)
- Sequential, Parallel, and Quantified Updates of First-Order Structures (Q5387908) (← links)
- Logics in Artificial Intelligence (Q5394151) (← links)
- Automated Deduction – CADE-20 (Q5394617) (← links)
- Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic (Q5423862) (← links)
- White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing (Q5423871) (← links)
- Model Checking of Extended OCL Constraints on UML Models in SOCLe (Q5428906) (← links)
- (Q5447372) (← links)
- Automated Reasoning with Analytic Tableaux and Related Methods (Q5479272) (← links)
- Valigator: A Verification Tool with Bound and Invariant Generation (Q5505564) (← links)
- Logical Aspects of Computational Linguistics (Q5706945) (← links)
- FM 2005: Formal Methods (Q5716885) (← links)
- A Generic Intermediate Representation for Verification Condition Generation (Q5743596) (← links)
- Abstract State Machines 2004. Advances in Theory and Practice (Q5901601) (← links)
- Integrated Formal Methods (Q5901611) (← links)
