皆様、
京大の末永です。12月8日（火）の 13:00 から 筑波大の海野さんに講演をお願いしています。 ご参加をお待ちしております。
末永幸平
--
日時：2015年12月8日（火） 13:00-14:00 場所：総合研究7号館情報3講義室 講演者：海野 広志（筑波大学大学院システム情報工学研究科コンピュータサイエンス専攻助教） 講演題目：帰納法によるホーン節制約解消法と関数型プログラムの関係的仕様自動検証への応用
概 要：Verification problems of programs in various paradigms (e.g. imperative, functional, and concurrent) can be reduced to constraint solving problems of Horn clauses over predicate variables, which represent unknown inductive invariants to be inferred. In this talk, we present a novel constraint solving method based on inductive theorem proving: the method reduces Horn constraint solving to validity checking of first-order formulas with inductively-defined predicates,which are then checked by induction on the derivation of the predicates. The method here uses an SMT solver to automate inductive proofs.
The main advantage of our constraint solving method over existing methods is that it can verify relational specifications (e.g., the equivalence, associativity, commutativity, distributivity, monotonicity, idempotency, and non-interference) where multiple function calls need to be analyzed simultaneously. Furthermore, our novel combination of Horn constraint solving and inductive theorem proving extends the reach of induction-based verification from pure total functions to impure partial procedures in various paradigms. We have implemented a prototype Horn constraint solver based on the proposed method and obtained promising results in preliminary experiments.