Cyclist
From MaRDI portal
Cited in
(43)- Compositional entailment checking for a fragment of separation logic
- CIRC
- Predator
- HipSpec
- Induction and Skolemization in saturation theorem proving
- Cyclic proofs, hypersequents, and transitive closure logic
- Transforming orthogonal inductive definition sets into confluent term rewrite systems
- Uniform interpolation from cyclic proofs: the case of modal mu-calculus
- SLAyer
- HIP
- PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points
- HERMIT
- VATA
- Combining induction and saturation-based theorem proving
- Circular proofs for the Gödel-Löb provability logic
- Inductive theorem proving based on tree grammars
- Soundness and completeness proofs by coinductive methods
- Automated mutual induction proof in separation logic
- Pesca
- THOR
- Model checking for symbolic-heap separation logic with inductive predicates
- Cyclic arithmetic is equivalent to Peano arithmetic
- Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
- Unified reasoning about robustness properties of symbolic-heap separation logic
- coreStar
- Jimple
- InKa
- Infer
- A3PAT
- Disproving inductive entailments in separation logic via base pair approximation
- Deciding entailments in inductive separation logic with tree automata
- QuodLibet
- Slide
- Program equivalence is coinductive
- Local validity for circular proofs in linear logic with fixed points
- Partial evaluation of string obfuscations for Java malware detection
- Clause set cycles and induction
- scientific article; zbMATH DE number 7155168 (Why is no real title available?)
- Classical system of Martin-Löf's inductive definitions is not equivalent to cyclic proofs
- Program Verification with Separation Logic
- Automatically verifying temporal properties of pointer programs with cyclic proof
- Sound and complete equational reasoning over comodels
- IsaCoSy
This page was built for software: Cyclist
