Logic-ml December 2015

9 participants
12 discussions

証明論研究集会 & SLACS のご案内
by Toshihiko Kurata 07 Dec '15

07 Dec '15

皆様，証明論研究集会とSLACSの講演申込みを有難うございました．暫定版プログラムなど詳しい情報はHP https://sites.google.com/site/ptslacs2015/ から御確認頂けたらと思います．現状で枠に若干の余裕が出来ましたので，埋まるまでの間は講演の募集を続けることとなりました．希望をされる方は申し込みを頂けますと幸いです．あと，都合により懇親会は月曜日に行うこととなりました．御不便をお掛けしますが，よろしくお願いいたします．佐々木克巳（南山大学）倉田俊彦（法政大学）

1 0

講演: 海野さん（筑波大）
by Kohei SUENAGA 05 Dec '15

05 Dec '15

皆様、京大の末永です。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(a)gmail.com http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml December 2015