Using Hypersafety Verification for Proving Correctness of Programming AssignmentsNIER
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 JulDisplayed time zone: (UTC) Coordinated Universal Time change
07:00 - 08:00 | I19-Code Generation and VerificationTechnical Papers / Software Engineering in Practice / New Ideas and Emerging Results at Baekje Chair(s): Raffi Khatchadourian City University of New York (CUNY) Hunter College | ||
07:00 6mTalk | Using Hypersafety Verification for Proving Correctness of Programming AssignmentsNIER New Ideas and Emerging Results Jude Anil TCS Research, Sumanth Prabhu TCS Research, Kumar Madhukar TCS Innovation Labs (TRDDC), R Venkatesh | ||
07:06 12mTalk | Automatically Testing String SolversTechnical Technical Papers Pre-print | ||
07:18 6mTalk | On the Power of Abstraction: a Model-Driven Co-evolution Approach of Software CodeNIER New Ideas and Emerging Results Djamel Eddine Khelladi CNRS, France, Benoit Combemale University of Toulouse and Inria, Mathieu Acher (Univ Rennes, Inria, IRISA), Olivier Barais (Univ Rennes, Inria, IRISA) | ||
07:24 12mTalk | Co-Evolving Code with Evolving MetamodelsTechnical Technical Papers Djamel Eddine Khelladi CNRS, France, Benoit Combemale University of Toulouse and Inria, Mathieu Acher (Univ Rennes, Inria, IRISA), Olivier Barais (Univ Rennes, Inria, IRISA), Jean-Marc Jézéquel Univ Rennes - IRISA | ||
07:36 12mTalk | Rule-based Code Generation in Industrial Automation: Four Large-scale Case Studies applying the CAYENNE MethodSEIP Software Engineering in Practice Heiko Koziolek ABB Corporate Research, Andreas Burger ABB Corporate Research, Marie Platenius-Mohr ABB Corporate Research, Julius Rückert ABB Corporate Research, Hadil Abukwaik ABB Corporate Research, Raoul Jetley ABB, Abdulla PP ABB Corporate Research Pre-print | ||
07:48 12mTalk | Understanding and Handling Alert Storm for Online Service SystemsSEIP Software Engineering in Practice Nengwen Zhao Tsinghua University, Junjie Chen Tianjin University, Xiao Peng China EverBright Bank, Honglin Wang BizSeer, Xinya Wu BizSeer, Yuanzong Zhang BizSeer, Zikai Chen Tsinghua University, Xiangzhong Zheng BizSeer, Xiaohui Nie Tsinghua University, Gang Wang China EverBright Bank, Yong Wu China EverBright Bank, Fang Zhou China EverBright Bank, Wenchi Zhang BizSeer, Kaixin Sui BizSeer, Dan Pei Tsinghua University |