Formal
Methods in
Software Engineering

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.

Examples