Wed 10 Jan 2018 14:55 - 15:20 at Bunker Hill - Verification I Chair(s): Zhong Shao

This paper considers verification of {\em non-deterministic} higher-order functional programs. Our contribution is a novel type system in which the types are used to express and verify (conditional) safety, termination, non-safety, and non-termination properties in the presence of $\forall$-$\exists$ branching behavior due to non-determinism. For instance, the judgement $\vdash e:{u:\mathtt{int}\mid\phi(u)}^{\forall\forall}$ says that every evaluation of $e$ either diverges or reduces to some integer $u$ satisfying $\phi(u)$, whereas $\vdash e:{u:\mathtt{int}\mid\psi(u)}^{\exists\forall}$ says that there exists an evaluation of $e$ that either diverges or reduces to some integer $u$ satisfying $\psi(u)$. Note that the former is a safety property whereas the latter is a counterexample to a (conditional) termination property. Following the recent work on type-based verification methods for deterministic higher-order functional programs, we formalize the idea on the foundation of {\em dependent refinement types}, thereby allowing the type system to express and verify rich properties involving program values, branching behaviors, and the combination thereof.

Our type system is able to seamlessly combine deductions of both universal and existential facts within a unified framework, paving the way for an exciting opportunity for new type-based verification methods that combine both universal and existential reasoning. For example, our system can prove the existence of a path violating some safety property from a proof of termination that uses a well-foundedness termination argument. We prove that our type system is sound and relatively complete, and further, thanks to having both modes of non-determinism, we show that our types are closed under complement.

Wed 10 Jan

Displayed time zone: Tijuana, Baja California change

13:40 - 15:20
Verification IResearch Papers at Bunker Hill
Chair(s): Zhong Shao Yale University
13:40
25m
Talk
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Research Papers
Quang-Trung Ta National University of Singapore, Ton Chanh Le National University of Singapore, Siau-Cheng Khoo National University of Singapore, Wei-Ngan Chin National University of Singapore
14:05
25m
Talk
Foundations for Natural Proofs and Quantifier Instantiation
Research Papers
Christof Löding RWTH Aachen University, P. Madhusudan University of Illinois at Urbana-Champaign, Lucas Peña University of Illinois at Urbana-Champaign
14:30
25m
Talk
Higher-Order Constrained Horn Clauses for Verification
Research Papers
Toby Cathcart Burn University of Oxford, C.-H. Luke Ong University of Oxford, Steven Ramsay University of Bristol
14:55
25m
Talk
Relatively Complete Refinement Type System for Verification of Higher-Order Non-Deterministic Programs
Research Papers
Hiroshi Unno University of Tsukuba, Yuki Satake University of Tsukuba, Tachio Terauchi Waseda University