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