[logic-ml] 講演会 (Nadia Polikarpova氏)

[Atsushi Igarashi]

皆様，

京都大学の五十嵐です．

以下の要領で MIT の Nadia Polikarpova さんの講演会を実施いたしますので，
ふるってご参加ください．当日夕方には，簡単な懇親会も考えておりますので，
興味のある方は五十嵐までご連絡ください．

どうぞよろしくお願いいたします
--
五十嵐 淳 (IGARASHI Atsushi)
E-mail: igarashi at kuis.kyoto-u.ac.jp
url: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/

----------------------------------------------------------------------

日時: ３月１２日(木) 14:00〜15:00
場所: 京都大学吉田キャンパス
      総合研究７号館(旧工学部１０号館)１階１３１号室(セミナー室２)

Title: A Fully Verified Container Library and Synthesis from Liquid Types

Abstract:

In this talk I will discuss two approaches to constructing provably
correct programs: one is based on automated deductive verification,
and the other one combines program synthesis and refinement types.

The first part of my talk will present AutoProof: an automated
deductive verifier for heap-manipulating object-oriented programs, as
well as our experience using AutoProof to prove full functional
correctness of a realistic general-purpose container library. While
the comprehensive functionality and flexible design of container
libraries pose nontrivial challenges to formal verification, our
results indicate that verifying a realistic library (135 public
methods, 8,400 LOC) is possible with moderate annotation overhead (1.4
lines of specification per LOC) and good performance (0.2 seconds per
method on average).

The second part of my talk builds upon the Liquid Types framework,
which has been successfully used to verify a wide range of properties
of functional programs with very little human interaction. The secret
to this success is the encoding of program invariants using a
combination of types and predicates from an SMT-decidable logic. I
will discuss some ideas on how Liquid Type inference could be extended
to infer program components, and ultimately synthesize programs that
are correct by construction.

Bio:

Nadia Polikarpova is a postdoctoral researcher at MIT, where she works
with Armando Solar-Lezama. She obtained her PhD at ETH Zurich in
2014. Her research interests are in program verification and
synthesis.