Try Circ Online

Jump to: navigation, search

(back to Circ main page)

You have reached the Circ online demo page. Please enter your specification in the form below, or chose (and possibly modify) one of the existing specifications. When you are done with editing the specification, click on Run. Upon completion, the proof will be displayed underneath the form.

  • Here is the main page of Circ, which contains links to papers, documentation, and source code
  • Here is a paper showing that the problem Circ is attempting to solve is \Pi_2^0-hard even in the special case of streams; in other words, one can always find proof tasks that Circ, or any prover for behavioral equivalence, will not be able to handle. We are, nevertheless, interested in knowing about these. Therefore, we are grateful if you let us know about your experience with Circ, especially if you have proof tasks that you think are easy but Circ cannot prove.

Note: at the beginning of each example you can uncomment the command (set show details on .) in order to see all the details of the proofs. You can do this by removing the three dashes preceding the command.

Choose an example:
  • coinduction
    • bitstream
      • bitstream
    • fieldstream
      • fieldstream
    • high-order
      • mapstr
    • infinite-binary-trees
      • infinite-binary-trees
    • natstream
      • natstream
      • rev3
    • processes
      • bisimilarity-kripke-eqn-ex2
      • bisimilarity-lts-eqn-ex1
      • bisimilarity-lts-rts-ex1
      • bpa
      • context-free-processes
    • regular-expressions
      • ere-with-simplification
      • ere
    • ringstream
      • assoc-comm-as-operational-goals
      • ringstream
    • treestream
      • treestream
  • induction
    • fib
    • list-mirrored-length
    • list-sum-length
    • maxlist
    • nat++
    • nat
    • oddeven
    • pa
    • tree
  • combine-ind-coind
 

Please press the Run button once and wait; it may take a few seconds to run Circ; the execution of Circ using this web interface is limited to 2 minutes of CPU time and 500 MB of RAM.

Personal tools
Namespaces

Variants
Views
Actions
Navigation