KIV

swMATH10060MaRDI QIDQ22029FDOQ22029

Author name not available (Why is that?)

Cited In (48)

• Refinement and retrenchment for programming language data types
• A complete axiom system for propositional interval temporal logic with infinite time
• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Automated Reasoning
• Algebraic Methodology and Software Technology
• Title not available (Why is that?)
• Proving linearizability with temporal logic
• Automating Algebraic Specifications of Non-freely Generated Data Types
• Completeness of fair ASM refinement
• Verifying Concurrent Systems with Symbolic Execution
• ASM refinement and generalizations of forward simulation in data refinement: a comparison
• Predicate abstraction in a program logic calculus
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages
• Fifty years of Hoare's logic
• Formal verification of a lock-free stack with hazard pointers
• Title not available (Why is that?)
• Title not available (Why is that?)
• A program logic for resources
• Compositional reasoning using intervals and time reversal
• Title not available (Why is that?)
• Bounded Relational Analysis of Free Data Types
• Automated flaw detection in algebraic specifications
• Relational concurrent refinement. II: Internal operations and outputs
• Title not available (Why is that?)
• The WAM case study: Verifying compiler correctness for Prolog with KIV
• Mechanized proofs of opacity: a comparison of two techniques
• Temporal Logic Verification of Lock-Freedom
• A sound and complete proof technique for linearizability of concurrent data structures
• Plagiator — A learning prover
• Verification of Java Programs with Generics
• ASM refinement preserving invariants
• One logic to use them all
• Interactive verification of concurrent systems using symbolic execution
• A Compiled Implementation of Normalization by Evaluation
• Atomic actions, and their refinements to isolated protocols
• Towards interactive verification of programmable logic controllers using modal Kleene algebra and KIV
• Specifying imperative ML-like programs using dynamic logic
• Verifying opacity of a transactional mutex lock
• Completeness of ASM refinement
• MUNCH -- automated reasoner for sets and multisets
• Verification of concurrent systems with VerCors
• Title not available (Why is that?)
• Correctness of efficient real-time model checking
• RAVEN: Real-time analyzing and verification environment
• Title not available (Why is that?)
• Formal fault tree analysis -- practical experiences
• Title not available (Why is that?)

This page was built for software: KIV