KeY
From MaRDI portal
Software:21946
swMATH9969MaRDI QIDQ21946FDOQ21946
Author name not available (Why is that?)
Cited In (50)
- Refinement and retrenchment for programming language data types
- Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics
- Second-Order Principles in Specification Languages for Object-Oriented Programs
- Verifying OpenJDK's sort method for generic collections
- Verifying Whiley programs with Boogie
- A Proof Assistant for Alloy Specifications
- White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing
- Automating Verification of Loops by Parallelization
- Reasoning About Loops Using Vampire in KeY
- Invariants Synthesis over a Combined Domain for Automated Program Verification
- Sequential, Parallel, and Quantified Updates of First-Order Structures
- A logic for secure memory access of abstract state machines
- Automated Deduction – CADE-20
- Title not available (Why is that?)
- Proof pearl: The KeY to correct and stable sorting
- Deductive verification of floating-point Java programs in KeY
- Simplify: a theorem prover for program checking
- Fundamental Approaches to Software Engineering
- Assertion-based slicing and slice graphs
- A program logic for resources
- Integrated Formal Methods
- Ensuring the correctness of lightweight tactics for JavaCard dynamic logic
- Abstract State Machines 2004. Advances in Theory and Practice
- A Generic Intermediate Representation for Verification Condition Generation
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- Mechanical inference of invariants for FOR-loops
- Gray-box monitoring of hyperproperties with an application to privacy
- Logical Aspects of Computational Linguistics
- Invariant-driven specifications in Maude
- A comparison of tools for teaching formal software verification
- Semantics, calculi, and analysis for object-oriented specifications
- Automated Reasoning with Analytic Tableaux and Related Methods
- Verification conditions for source-level imperative programs
- A Universal Machine for Biform Theory Graphs
- KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
- Understanding parameters of deductive verification: an empirical investigation of KeY
- Valigator: A Verification Tool with Bound and Invariant Generation
- Formal specification and verification of JDK's identity hash map implementation
- Logics in Artificial Intelligence
- Could We Have Chosen a Better Loop Invariant or Method Contract?
- FM 2005: Formal Methods
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- Principled Software Development
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- Model Checking of Extended OCL Constraints on UML Models in SOCLe
- A verification-driven framework for iterative design of controllers
- Modular invariants for layered object structures
- Uniform substitution at one Fell swoop
- Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
- Title not available (Why is that?)
This page was built for software: KeY
