Cyclist

swMATH18519MaRDI QIDQ30358FDOQ30358

Author name not available (Why is that?)

Source code repository: https://github.com/ngorogiannis/cyclist

Cited In (26)

• 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
• Title not available (Why is that?)
• Program Equivalence is Coinductive
• Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
• Deciding Entailments in Inductive Separation Logic with Tree Automata
• Transforming orthogonal inductive definition sets into confluent term rewrite systems
• Program Verification with Separation Logic
• Disproving Inductive Entailments in Separation Logic via Base Pair Approximation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Soundness and completeness proofs by coinductive methods
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points
• 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
• Induction and Skolemization in saturation theorem proving
• Cyclic proofs, hypersequents, and transitive closure logic
• Cyclic Arithmetic Is Equivalent to Peano Arithmetic
• Sound and complete equational reasoning over comodels
• Title not available (Why is that?)
• Combining induction and saturation-based theorem proving
• Inductive theorem proving based on tree grammars

This page was built for software: Cyclist