ICE-TCS Lectures Series - Eugen-Ioan Goriac - CIRC: A Behavioral Verification Tool based on Circular Coinduction

The next ICE-TCS  talk will be delivered on Friday, 13 August, by Eugen-Ioan Goriac (Reykjavik University). The talk, which is entitled CIRC: A Behavioral Verification Tool based on Circular Coinduction, will be held at 14:00 in room M1.05 at the new premises of Reykjavik University in Nauthólsvík.

Eugen-Ioan Goriac has recently joined ICE-TCS as a PhD student.

Everyone is welcome.


CIRC is a tool for automated coinductive theorem proving. It includes an engine based on circular coinduction, which makes it particularly well-suited for proving behavioral properties of infinite data-structures. Circular coinduction is an automated process that, when provided a set of goals (proof obligations), runs according to the strategy: "((reduce one goal) or-else (derive new goals from one goal)) for as long as possible". When no more goals are left to be proved CIRC stops, and at that moment it is sound to conclude that the initial set of goals hold.