Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 12:00 - 12:30 at PEPM - Session 2 Chair(s): Youyou Cong

Type-based program verification, which reduces program verification to type inference, has been used as a lightweight approach to automated program verification. Whilst it is often effective and faster than other methods such as model checking, the type-based approach often fails to provide useful information upon a failure of the verification. We address this problem for a recent type-based verification tool called ConSORT for imperative programs. Producing a useful error message is particularly challenging for ConSORT, as the underlying type system combines the notions of ownership, refinement types, and context-sensitivity. This paper pro- poses a method to produce error messages for ConSORT and reports an implementation and experimental results. The proposed method is potentially useful also for other type-based tools for automated program verification.

Mon 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:30 - 12:30: Session 2PEPM at PEPM
Chair(s): Youyou CongTokyo Institute of Technology

Live stream: https://www.youtube.com/watch?v=tuxm51MLkHM

11:30 - 12:00
Research paper
Coq to C Translation with Partial Evaluation
Akira TanakaNational Institute of Advanced Industrial Science and Technology (AIST)
Media Attached
12:00 - 12:30
Research paper
Counterexample Generation for Program Verification based on Ownership Refinement TypesBest Paper Award
Hideto UenoThe Univeristy of Tokyo, John TomanCertora, inc., Naoki KobayashiUniversity of Tokyo, Japan, Takeshi TsukadaChiba University, Japan
Media Attached