Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 17:00 - 17:30 at Sala X - Session 3 Chair(s): Atsushi Igarashi

There have been two major approaches to fully automated verification of higher-order functional programs: higher-order model checking and refinement type inference. The former approach is precise, but suffers from a bottleneck in the predicate discovery phase. The latter approach is generally faster than the former, thanks to the recent advances in constrained Horn clause (CHC) solving, but is imprecise, in that it rejects some valid programs. To take the best of the two approaches, we refine the higher-order model checking approach, by employing CHC solving in the predicate discovery phase. We have implemented the new approach and confirmed that the new system can verify more programs than those based on the previous two approaches.

Mon 14 Jan
Times are displayed in time zone: (GMT+01:00) Greenwich Mean Time : Belfast change

16:00 - 17:30: PEPM 2019 - Session 3 at Sala X
Chair(s): Atsushi IgarashiKyoto University, Japan
pepm-2019-papers16:00 - 17:00
Jens PalsbergUniversity of California, Los Angeles (UCLA)
File Attached
pepm-2019-papers17:00 - 17:30
Ryosuke SatoKyushu University, Japan, Naoki IwayamaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan