An update for CITP

Daniel Gaina

Date:	2014/08/28 (Thu) 15:00 to 17:00
Place:	Seminar room 9th floor
Group:	Research Center for Software Verification

Constructor-based Inductive Theorem Prover (CITP) is a tool for proving inductive properties of software systems specified with constructor-based logics. We extend the methodology supported by CITP to prove invariant properties of observational transitional systems (OTS) specified with transition rules. We also discuss issues related to implementation and future direction of research.

Contact	nao-aoki