皆様，

京都大学の五十嵐です．

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

どうぞよろしくお願いいたします -- 五十嵐 淳 (IGARASHI Atsushi) E-mail: [email protected] 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.