# Try Circ Online

(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.