Cited in
(65)- scientific article; zbMATH DE number 1390241 (Why is no real title available?)
- Formal fault tree analysis -- practical experiences
- Refinement and retrenchment for programming language data types
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- A complete axiom system for propositional interval temporal logic with infinite time
- Automated Reasoning
- Algebraic Methodology and Software Technology
- Proving linearizability with temporal logic
- Completeness of fair ASM refinement
- ASM refinement and generalizations of forward simulation in data refinement: a comparison
- Automating Algebraic Specifications of Non-freely Generated Data Types
- scientific article; zbMATH DE number 1948197 (Why is no real title available?)
- Verifying Concurrent Systems with Symbolic Execution
- Predicate abstraction in a program logic calculus
- \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages
- Abstract Interpretation of Symbolic Execution with Explicit State Updates
- Fifty years of Hoare's logic
- Formal verification of a lock-free stack with hazard pointers
- scientific article; zbMATH DE number 4074539 (Why is no real title available?)
- scientific article; zbMATH DE number 1566286 (Why is no real title available?)
- A program logic for resources
- Compositional reasoning using intervals and time reversal
- scientific article; zbMATH DE number 827984 (Why is no real title available?)
- Bounded Relational Analysis of Free Data Types
- Automated flaw detection in algebraic specifications
- ALGOL 68
- CoFI
- AutoBayes/CC
- PLAGIATOR
- FINDER
- MUNCH
- PAF!
- RAVEN
- TLPVS
- RGITL
- Grail
- Line-up
- NOrec
- RingSTM
- Camelot
- DOVE
- ABSFOL
- Relational concurrent refinement. II: Internal operations and outputs
- Mechanized proofs of opacity: a comparison of two techniques
- scientific article; zbMATH DE number 1678385 (Why is no real title available?)
- The WAM case study: Verifying compiler correctness for Prolog with KIV
- Temporal Logic Verification of Lock-Freedom
- A sound and complete proof technique for linearizability of concurrent data structures
- Plagiator — A learning prover
- ASM refinement preserving invariants
- Verification of Java Programs with Generics
- A Compiled Implementation of Normalization by Evaluation
- Interactive verification of concurrent systems using symbolic execution
- Atomic actions, and their refinements to isolated protocols
- One logic to use them all
- 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
- scientific article; zbMATH DE number 2003150 (Why is no real title available?)
- Correctness of efficient real-time model checking
- RAVEN: Real-time analyzing and verification environment
- scientific article; zbMATH DE number 1552510 (Why is no real title available?)
This page was built for software: KIV
