Blogs (1) >>
ASE 2019
Sun 10 - Fri 15 November 2019 San Diego, California, United States
Wed 13 Nov 2019 13:40 - 14:00 at Cortez 1 - Verification and Bug Detection Chair(s): Raghavan Komondoor

Mutation analysis, which introduces artificial defects into software systems, is the basis of mutation testing, a technique widely applied to evaluate and enhance the quality of test suites. However, despite the deep analogy between tests and formal proofs, mutation analysis has seldom been considered in the context of deductive verification. We propose mutation proving, a technique for analyzing verification projects that use proof assistants. We implemented our technique for the Coq proof assistant in a tool dubbed mCoq. mCoq applies a set of mutation operators to Coq definitions of functions and datatypes, inspired by operators previously proposed for functional programming languages. mCoq then checks proofs of lemmas affected by operator application. To make our technique feasible in practice, we implemented several optimizations in mCoq such as parallel proof checking. We applied mCoq to several medium and large scale Coq projects, and recorded whether proofs passed or failed when applying different mutation operators. We then qualitatively analyzed the mutants, and found several examples of weak and incomplete specifications. For our evaluation, we made many improvements to serialization of Coq code and even discovered a notable bug in Coq itself, all acknowledged by developers. We believe mCoq can be useful both to proof engineers for improving the quality of their verification projects and to researchers for evaluating proof engineering techniques.

Conference Day
Wed 13 Nov

Displayed time zone: Tijuana, Baja California change

13:40 - 15:20
Verification and Bug DetectionDemonstrations / Research Papers at Cortez 1
Chair(s): Raghavan KomondoorIndian Institute of Science, Bangalore
13:40
20m
Talk
Mutation Analysis for Coq
Research Papers
Ahmet CelikThe University of Texas at Austin, Karl PalmskogUniversity of Texas at Austin, Marinela ParovicThe University of Texas at Austin, Emilio Jesús Gallego AriasMINES ParisTech, Milos GligoricThe University of Texas at Austin
14:00
20m
Talk
Verifying Arithmetic in Cryptographic C Programs
Research Papers
Jiaxiang LiuShenzhen University, Xiaomu ShiShenzhen University, Ming-Hsien TsaiAcademia Sinica, Taiwan, Bow-Yaw WangAcademia Sinica, Bo-Yin YangAcademia Sinica
Pre-print
14:20
20m
Talk
Model checking embedded control software using OS-in-the-loop CEGAR
Research Papers
Dongwoo KimKyungpook National University, Yunja ChoiKyungpook National University
Pre-print
14:40
20m
Talk
Get rid of inline assembly through verification-oriented lifting
Research Papers
Frédéric RecoulesCEA LIST, Sébastien BardinCEA LIST, Richard BonichonCEA LIST, Laurent MounierUniversité Grenoble Alpes, Marie-Laure PotetUniversité Grenoble Alpes
DOI Pre-print
15:00
10m
Demonstration
VeriAbs : Verification by Abstraction and Test Generation
Demonstrations
Mohammad AfzalTata Cosultancy Services, A AsiaTata Cosultancy Services, Avriti ChauhanTata Cosultancy Services, Bharti ChimdyalwarTata Consultancy Services, Priyanka DarkeTata Consultancy Services, Advaita DatarTata Consultancy Services Ltd, Shrawan KumarTata Cosultancy Services, R VenkateshTata Research Development and Design Centre
15:10
10m
Demonstration
SGUARD: A Feature-based Clustering Tool for Effective Spreadsheet Defect Detection
Demonstrations
Da LiState Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University, Nanjing, China, Huiyan WangState Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University, Nanjing, China, Chang XuNanjing University, Ruiqing ZhangSearch Tech. Center Asia, Microsoft, Suzhou, China, Shing-Chi CheungDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiaoxing MaState Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University