Write a Blog >>
Fri 13 Nov 2020 01:39 - 01:40 at Virtual room 2 - SAT and Synthesis

Deciding termination of programs is probably the most famous problem in computer science. Synthesizing ranking functions for programs is a standard way to prove termination of programs. Currently, specific synthesis algorithms have to be developed for each specific type of programs. For instance, the synthesis of ranking functions for programs with linear variables updates is usually based on linear programming techniques and the like, while for programs with polynomial updates, it usually relies on semi-definite programming and the like. The same also applies to the synthesis of different types of ranking functions needed for proving program termination. Each time faced with a new type of programs and a new type of ranking functions, researchers have to spend a considerable amount of effort to develop specialized synthesis algorithms. In this paper, to save this extra effort, we present \textsc{SVMRanker}, a general framework for proving termination of programs, which is able to synthesize different types of ranking functions for programs with both linear and polynomial updates, based on Support-Vector Machines (SVM). We compare \textsc{SVMRanker} with the state-of-the-art tool \textsc{LassoRanker} on standard benchmarks. Empirical results show that \textsc{SVMRanker} is comparable with \textsc{LassoRanker} on programs with linear updates and can manage more programs with polynomial updates, making \textsc{SVMRanker} a valid complement to \textsc{LassoRanker} in proving program termination.

Fri 13 Nov
Times are displayed in time zone: (UTC) Coordinated Universal Time change

01:30 - 02:00: SAT and SynthesisPaper Presentations / Research Papers / Tool Demos at Virtual room 2
01:30 - 01:32
Talk
Tool Demos
Jiayi YangUniversity of Texas at Austin, USA, Wenxi WangUniversity of Texas at Austin, USA, Darko MarinovUniversity of Illinois at Urbana-Champaign, Sarfraz KhurshidUniversity of Texas at Austin
DOI
01:32 - 01:34
Talk
Research Papers
Zifan NanNorth Carolina State University, USA, Hui GuanUniversity of Massachusetts at Amherst, USA, Xipeng ShenNorth Carolina State University, USA
DOI
01:35 - 01:36
Talk
Research Papers
Shivam HandaMassachusetts Institute of Technology, USA, Martin RinardMassachusetts Institute of Technology, USA
DOI
01:37 - 01:38
Talk
Tool Demos
Abtin MolaviHarvey Mudd College, USA, Mara DowningHarvey Mudd College, USA, Tommy SchneiderHarvey Mudd College, USA, Lucas BangHarvey Mudd College
DOI
01:39 - 01:40
Talk
Tool Demos
Xie Li, Yi LiNanyang Technological University, Singapore, Yong LiInstitute of Software, Chinese Academy of Sciences, Xuechao SunInstitute of Software at Chinese Academy of Sciences, China, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of Sciences
DOI
01:41 - 02:00
Talk
Paper Presentations
Abtin MolaviHarvey Mudd College, USA, Jiayi YangUniversity of Texas at Austin, USA, Lucas BangHarvey Mudd College, Xie Li, Zifan NanNorth Carolina State University, USA, Shivam HandaMassachusetts Institute of Technology, USA, M: Abhik RoychoudhuryNational University of Singapore, Singapore