[logic-ml] 講演: 海野さん（筑波大）

[Kohei SUENAGA]

皆様、

京大の末永です。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.

-- 
Kohei Suenaga (末永幸平), Ph.D
Associate professor (准教授)
Graduate School of Informatics, Kyoto University
(京都大学情報学研究科)
ksuenaga at gmail.com
http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/