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
• Specifying Imperative ML-Like Programs Using Dynamic Logic
• Title not available (Why is that?)
• Proving linearizability with temporal logic
• Automating Algebraic Specifications of Non-freely Generated Data Types
• Towards Interactive Verification of Programmable Logic Controllers Using Modal Kleene Algebra and KIV
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• A program logic for resources
• One Logic to Use Them All
• Compositional reasoning using intervals and time reversal
• Title not available (Why is that?)
• Bounded Relational Analysis of Free Data Types
• Verifying Opacity of a Transactional Mutex Lock
• Automated flaw detection in algebraic specifications
• Relational concurrent refinement. II: Internal operations and outputs
• Completeness of ASM Refinement
• Verification of Concurrent Systems with VerCors
• Formal Verification of a Lock-Free Stack with Hazard Pointers
• Formal Fault Tree Analysis - Practical Experiences
• 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
• MUNCH - Automated Reasoner for Sets and Multisets
• Temporal Logic Verification of Lock-Freedom
• Plagiator — A learning prover
• Verification of Java Programs with Generics
• ASM refinement preserving invariants
• Interactive verification of concurrent systems using symbolic execution
• A Compiled Implementation of Normalization by Evaluation
• Atomic actions, and their refinements to isolated protocols
• Title not available (Why is that?)
• A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
• Correctness of efficient real-time model checking
• RAVEN: Real-time analyzing and verification environment
• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for software: KIV