[logic-ml] Prof. Aleksy Schubert at NII Logic Seminar

[Makoto Tatsuta]

	      Prof. Aleksy Schubert at NII Logic Seminar


Date: September 26, 2014, 14:00--16:00

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

Speaker: Prof. Aleksy Schubert (University of Warsaw)

(1) 
Title: Undecidability and complexity in fragments of first-order
intuitionistic logic

Abstract: 
In case of classical first-order logic there is a full
characterisation of decidable and undecidable classes of formulae
depending on the quantifier prefix and the vocabulary that is
used. First-order logic in intuitionistic case lacks this kind of
classification since there is no prefix normal form and actually the
prenex fragment of the logic is in many cases much weaker than the
general calculus. However, there is one meaningful stratification of
the intuitionistic logic similar to the prenex form. We can consider
classes of formulae that would result in a particular prefix of
quantifiers when transformed using classical equivalences. The status
of decidable and undecidable cases within this stratification will be
presented as well as the complexity of known subcases.

(2) 
Title: Verification of programs using Frama-C and Why3

Abstract:
Frama-C is a tool that makes it possible to do a variety of analyses
for C programs annotated with C specification language called ACSL
(The ANSI/ISO C Specification Langage). One of the possible ways to
use Frama-C is to generate verification conditions for appropriately
defined Hoare logic that is in line with C programming language
semantics. These verification conditions can subsequently be
discharged by Why3 tool that makes it possible to manage the proving
of necessary properties. During the talk I will present an overview of
the tools and show a number of interesting examples to demonstrate how
these tools work together to make possible verification of practical
programs.

問合せ先:
龍田 真 (国立情報学研究所)
e-mail: tatsuta at nii.ac.jp
http://research.nii.ac.jp/~tatsuta