Lecture by Sylvain Salvati at NII Logic Seminar

Date and Time: July 1, 16:00-17:00

Place: National Institute of Informatics, Conference Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/)

Speaker: Sylvain Salvati (INRIA Bordeaux Sud-Ouest)

Title: Model construction for higher-order model-checking

Abstract:

When dealing with finite state properties, it is usual to have some finite algebraic structures (e.g. finite monoids in the case of finite state automata on strings) that represent those properties. When dealing with logical properties of programs that are computed by finite state automaton, the question of what is an "adequate" finite algebraic structure arises. Having such a structure would entail a sort of modularity in program verification, but it also gives some strong understanding of how the properties can be checked.

In the context of higher-order verification, programs are models as lambda-terms and it is natural to think about denotational domains as a possible candidate. Finitary Scott domains only capture very simple properties of the Bohm trees generated by higher-order programs. This talk will illustrate how to enrich Scott domains so that they can capture wider classes of finite state properties.

問合せ先: 金沢 誠 (国立情報学研究所) e-mail: [email protected]