Cyclist

Cyclist is a framework for building cyclic theorem provers based on a sequent calculus. In addition, over the years several decision procedures or algorithms have been integrated, focusing on Separation Logic with inductively defined predicates. For information on building Cyclist, the available tools included and the papers underpinning those tools, visit www.cyclist-prover.org


References in zbMATH (referenced in 20 articles )

Showing results 1 to 20 of 20.
Sorted by year (citations)

  1. Das, Anupam: On the logical complexity of cyclic arithmetic (2020)
  2. Echenim, M.; Peltier, N.: Combining induction and saturation-based theorem proving (2020)
  3. Tellez, Gadi; Brotherston, James: Automatically verifying temporal properties of pointer programs with cyclic proof (2020)
  4. Berardi, Stefano; Tatsuta, Makoto: Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proofs (2019)
  5. Nollet, Rémi; Saurin, Alexis; Tasson, Christine: PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points (2019)
  6. Ta, Quang-Trung; Le, Ton Chanh; Khoo, Siau-Cheng; Chin, Wei-Ngan: Automated mutual induction proof in separation logic (2019)
  7. Berardi, Stefano; Tatsuta, Makoto: Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system (2017)
  8. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Soundness and completeness proofs by coinductive methods (2017)
  9. Chawdhary, Aziem; Singh, Ranjeet; King, Andy: Partial evaluation of string obfuscations for Java malware detection (2017)
  10. Enea, Constantin; Lengál, Ondřej; Sighireanu, Mihaela; Vojnar, Tomáš: Compositional entailment checking for a fragment of separation logic (2017)
  11. Jansen, Christina; Katelaan, Jens; Matheja, Christoph; Noll, Thomas; Zuleger, Florian: Unified reasoning about robustness properties of symbolic-heap separation logic (2017)
  12. Simpson, Alex: Cyclic arithmetic is equivalent to Peano arithmetic (2017)
  13. Brotherston, James; Gorogiannis, Nikos; Kanovich, Max; Rowe, Reuben: Model checking for symbolic-heap separation logic with inductive predicates (2016)
  14. Pattinson, Dirk; Schröder, Lutz: Program equivalence is coinductive (2016)
  15. Brotherston, James; Gorogiannis, Nikos: Disproving inductive entailments in separation logic via base pair approximation (2015)
  16. Eberhard, Sebastian; Hetzl, Stefan: Inductive theorem proving based on tree grammars (2015)
  17. Pattinson, Dirk; Schröder, Lutz: Sound and complete equational reasoning over comodels (2015)
  18. Iosif, Radu; Rogalewicz, Adam; Vojnar, Tomáš: Deciding entailments in inductive separation logic with tree automata (2014)
  19. Shamkanov, D. S.: Circular proofs for the Gödel-Löb provability logic (2014)
  20. Brotherston, James; Gorogiannis, Nikos; Petersen, Rasmus L.: A generic cyclic theorem prover (2012) ioport