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
- White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing
- Automating Verification of Loops by Parallelization
- Sequential, Parallel, and Quantified Updates of First-Order Structures
- A logic for secure memory access of abstract state machines
- Automated Deduction – CADE-20
- Proof pearl: The KeY to correct and stable sorting
- Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018
- KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
- Deductive verification of floating-point Java programs in KeY
- Simplify: a theorem prover for program checking
- Fundamental Approaches to Software Engineering
- A universal machine for biform theory graphs
- 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
- 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
- A verifying compiler for a multi-threaded object-oriented language
- Verification conditions for source-level imperative programs
- 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
- A generic intermediate representation for verification condition generation
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- Reasoning about loops using Vampire in KeY
- Model Checking of Extended OCL Constraints on UML Models in SOCLe
- A verification-driven framework for iterative design of controllers
- A proof assistant for Alloy specifications
- Modular invariants for layered object structures
- Uniform substitution at one Fell swoop
- Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
- Invariants synthesis over a combined domain for automated program verification
- Title not available (Why is that?)
This page was built for software: KeY
