Write a Blog >>
ASE 2020
Mon 21 - Fri 25 September 2020 Melbourne, Australia
Tue 22 Sep 2020 03:00 - 03:10 at Koala - Formal Methods (1) Chair(s): Nazareno Aguirre

We propose a novel approach to proving the termination of imperative programs by k-induction. By our approach, the termination proving problem can be formalized as a k-inductive invariant synthesis task. On the one hand, k-induction uses weaker invariants than that required by the standard inductive approach. On the other hand, the base case of k-induction, which unrolls the program, can provide stronger pre-condition for invariant synthesis. As a result, the termination arguments of our approach can be synthesized more efficiently than the standard method. We implement a prototype of our k-inductive approach. The experimental results show the significant effectiveness and efficiency of our approach.

Tue 22 Sep
Times are displayed in time zone: (UTC) Coordinated Universal Time

02:20 - 03:20: Formal Methods (1)Research Papers / NIER track at Koala
Chair(s): Nazareno AguirreDept. of Computer Science FCEFQyN, University of Rio Cuarto
02:20 - 02:40
Accelerating All-SAT Computation with Short Blocking Clauses
Research Papers
Yueling ZhangSingapore Management University, Geguang PuEast China Normal University, Jun SunSingapore Management University
02:40 - 03:00
A Predictive Analysis for Detecting Deadlock in MPI Programs
Research Papers
Yu HuangSouthwestern University of Finance and Economics, Benjamin OglesBrigham Young University, Eric MercerBrigham Young University
03:00 - 03:10
Proving Termination by k-Induction
NIER track
Jianhui ChenTsinghua University, Fei HeTsinghua University, China