swMATH18519MaRDI QIDQ30358FDOQ30358
Author name not available (Why is that?)
Official website: http://www.cyclist-prover.org
Source code repository: https://github.com/ngorogiannis/cyclist
Cited In (43)
- 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
- IsaCoSy
- Title not available (Why is that?)
- Local validity for circular proofs in linear logic with fixed points
- Transforming orthogonal inductive definition sets into confluent term rewrite systems
- Program Verification with Separation Logic
- Title not available (Why is that?)
- Soundness and completeness proofs by coinductive methods
- CIRC
- Predator
- HipSpec
- HIP
- SLAyer
- HERMIT
- VATA
- Pesca
- THOR
- Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
- coreStar
- Jimple
- InKa
- Infer
- A3PAT
- QuodLibet
- Slide
- Cyclic arithmetic is equivalent to Peano arithmetic
- PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points
- 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
- Sound and complete equational reasoning over comodels
- Combining induction and saturation-based theorem proving
- Inductive theorem proving based on tree grammars
- Unified reasoning about robustness properties of symbolic-heap separation logic
This page was built for software: Cyclist
