Write a Blog >>
ICSE 2020
Wed 24 June - Thu 16 July 2020
Fri 10 Jul 2020 07:00 - 07:06 at Baekje - I19-Code Generation and Verification Chair(s): Raffi Khatchadourian

We look at the problem of deciding correctness of a programming assignment submitted by a student, with respect to a reference implementation provided by the teacher, the correctness property being output equivalence of the two programs. Typically, programming assignments are evaluated against a set of test-inputs. This checks for output equivalence, but limited to the cases that have been tested for. One may compose the programs sequentially and assert at the end that the outputs must match. But verifying such programs is not easy; the proofs often require that the functionality of every component program be captured fully, making invariant inference a challenge. One may discover mismatches (i.e., bugs) using a bounded model checker, but their absence brings us back to the question of verification. In this paper, we show how a hypersafety verification technique can effectively be used for verifying correctness of programming assignments. This connects two seemingly unrelated problems, and opens up the possibility of employing tools and techniques being developed for the former to efficiently address the latter. We demonstrate the practicability of this approach by using a hypersafety verification tool named \emph{weaver} and several sample assignment problems.

Fri 10 Jul
Times are displayed in time zone: (UTC) Coordinated Universal Time change

icse-2020-paper-presentations
07:00 - 08:00: Paper Presentations - I19-Code Generation and Verification at Baekje
Chair(s): Raffi KhatchadourianCity University of New York (CUNY) Hunter College
icse-2020-New-Ideas-and-Emerging-Results07:00 - 07:06
Talk
Jude AnilTCS Research, Sumanth PrabhuTCS Research, Kumar MadhukarTCS Innovation Labs (TRDDC), R Venkatesh
icse-2020-papers07:06 - 07:18
Talk
Alexandra BugariuETH Zurich, Peter MüllerETH Zurich
Pre-print
icse-2020-New-Ideas-and-Emerging-Results07:18 - 07:24
Talk
Djamel Eddine KhelladiCNRS, France, Benoit CombemaleUniversity of Toulouse and Inria, Mathieu Acher(Univ Rennes, Inria, IRISA), Olivier Barais(Univ Rennes, Inria, IRISA)
icse-2020-papers07:24 - 07:36
Talk
Djamel Eddine KhelladiCNRS, France, Benoit CombemaleUniversity of Toulouse and Inria, Mathieu Acher(Univ Rennes, Inria, IRISA), Olivier Barais(Univ Rennes, Inria, IRISA), Jean-Marc JézéquelUniv Rennes - IRISA
icse-2020-Software-Engineering-in-Practice07:36 - 07:48
Talk
Heiko KoziolekABB Corporate Research, Andreas BurgerABB Corporate Research, Marie Platenius-MohrABB Corporate Research, Julius RückertABB Corporate Research, Hadil AbukwaikABB Corporate Research, Raoul JetleyABB, Abdulla PPABB Corporate Research
Pre-print
icse-2020-Software-Engineering-in-Practice07:48 - 08:00
Talk
Nengwen ZhaoTsinghua University, Junjie ChenTianjin University, Xiao PengChina EverBright Bank, Honglin WangBizSeer, Xinya WuBizSeer, Yuanzong ZhangBizSeer, Zikai ChenTsinghua University, Xiangzhong ZhengBizSeer, Xiaohui NieTsinghua University, Gang WangChina EverBright Bank, Yong WuChina EverBright Bank, Fang ZhouChina EverBright Bank, Wenchi ZhangBizSeer, Kaixin SuiBizSeer, Dan PeiTsinghua University