IFIP Logo
Sign in for Members and Observers

IFIP WG1.3 Foundations of System Specification


Talk "An Overview of Recent Research Activities around CafeOBJ "

by Kokichi Futatsugi

Sat, 03 September 2011 at 10:00 am in Winchester, United Kingdom

Abstract: This talk gives an overview of recent research activities around CafeOBJ formal specification language system. <BR><BR> After giving some introductory remarks on formal methods, CafeOBJ, and proof scores, two major approaches of combining inference (a la theorem proving) and search (a la model checking) in verifications with proof scores are explained with instructive simple examples. The one is a sort of typical combination of abstraction which is proved by inference with proof score and search of limited state space after the abstraction. The other is combination of backward search (with inference) and forward search (with search) in finding counter-examples which is called Induction Guided Falsification. <BR><BR> An important theoretical achievement of formalization of sound and "complete" proof rules which underlie the proof score method is also explained. <BR><BR> URL of related papers and presentation: <BR><BR> <A HREF="http://scholar.google.com/scholar?q=%22Fostering+Proof+Scores+in+CafeOBJ.%22">related paper 1</a>, <A HREF="http://www.jaist.ac.jp/~kokichi/talk/icfem2010/">web page for presentation of paper 1</a>, <A HREF="http://scholar.google.com/scholar?q=%22A+Combination+of+Forward+and+Backward+Reachability+Analysis+Methods.%22">related paper 2</a>

Slides