swMATH10060MaRDI QIDQ22029FDOQ22029
Author name not available (Why is that?)
Official website: http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/kiv/
Cited In (65)
- Verification of Java Programs with Generics
- Title not available (Why is that?)
- 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
- ALGOL 68
- CoFI
- AutoBayes/CC
- PLAGIATOR
- FINDER
- MUNCH
- PAF!
- RAVEN
- TLPVS
- RGITL
- Grail
- Line-up
- NOrec
- RingSTM
- Camelot
- DOVE
- ABSFOL
- 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
- 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
This page was built for software: KIV
