JAIST Logic@JAIST

An update for the Constructor-based Inductive Theorem Prover (CITP)

  • Daniel Gaina
Date: 2014/11/20 (Thu) 15:00 to 17:00
Place: JAIST IS school collaboration room 7 (5F)
Group: Research Center for Software Verification
Abstract: 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 transitional rules. We also discuss issues related to implementation and future directions of research.
Contact nao-aoki