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