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