Wed 13 Nov 2019 15:00 - 15:10 at Cortez 1 - Verification and Bug Detection Chair(s): Raghavan Komondoor
Verification of programs continues to be a challenge and no single technique succeeds on all programs. In this paper we present VeriAbs, a reachability C program verifier that incorporates a portfolio of techniques implemented as four strategies, where a strategy is a set of techniques applied in a specific sequence. It selects a strategy based on the kind of loops in the program. We analysed the effectiveness of implemented strategies on the 3831 verification tasks from the ReachSafety category of the 8th International Competition on Software Verification (SV-COMP) 2019 and found that although simple classic techniques - explicit state model checking and bounded model checking, succeed on a majority of the programs, a wide range of further techniques are required to analyse the rest. A screencast of the tool is available at https://youtu.be/YHxB2V4U0gQ.
Tue 12 Nov
10:00 - 10:40 Demonstration | Pangolin: An SFL-based Toolset for Feature Localization Bruno Miguel Sotto-Mayor de Castro MachadoIST, University of Lisbon, Alexandre PerezPalo Alto Research Center, Rui AbreuInstituto Superior Técnico, U. Lisboa & INESC-ID | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | A Quantitative Analysis Framework for Recurrent Neural Network Xiaoning DuNanyang Technological University, Xiaofei XieNanyang Technological University, Yi LiNanyang Technological University, Lei MaKyushu University, Yang LiuNanyang Technological University, Singapore, Jianjun ZhaoKyushu University | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | Ares: Inferring Error Specifications through Static Analysis Li ChiTsinghua University, Zuxing GuSchool of Software, Tsinghua University, Min ZhouTsinghua University, Ming GuTsinghua University, Hongyu ZhangThe University of Newcastle | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | SiMPOSE - Configurable N-Way Program Merging Strategies for Superimposition-based Analysis of Variant-Rich Software Dennis ReulingSoftware Engineering Group, University of Siegen, Udo KelterSoftware Engineering Group, University of Siegen, Sebastian RulandTU Darmstadt, Real-time Systems Lab, Malte LochauTU Darmstadt Pre-print Media Attached File Attached | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | VeriAbs : Verification by Abstraction and Test Generation 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 | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | DeepHunter: A Coverage-Guided Fuzzer for Deep Neural Networks Xiaofei XieNanyang Technological University, Hongxu ChenNanyang Technological University, Yi LiNanyang Technological University, Lei MaKyushu University, Yang LiuNanyang Technological University, Singapore, Jianjun ZhaoKyushu University | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | SPrinter: A Static Checker for Finding Smart Pointer Errors in C++ Programs Xutong MaInstitute of Software, Chinese Academy of Sciences, Jiwei YanInstitute of Software, Chinese Academy of Sciences, Yaqi LiInstitute of Software, Chinese Academy of Sciences, Jun YanInstitute of Software, Chinese Academy of Sciences, Jian ZhangInstitute of Software, Chinese Academy of Sciences | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | LIRAT: Layout and Image Recognition Driving Automated Mobile Testing of Cross-Platform Shengcheng YuNanjing University, China, Chunrong FangNanjing University, Yang FengUniversity of California, Irvine, Wenyuan ZhaoNanjing University, Zhenyu ChenNanjing University | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | FogWorkflowSim: An Automated Simulation Toolkit for Workflow Performance Evaluation in Fog Computing Xiao LiuSchool of Information Technology, Deakin University, Lingmin FanSchool of Computer Science and Technology, Anhui University, Jia XuSchool of Computer Science and Technology, Anhui University, Xuejun LiSchool of Computer Science and Technology, Anhui University, Lina GongSchool of Computer Science and Technology, Anhui University, John GrundyMonash University, Yun YangSwinburne University of Technology | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | SGUARD: A Feature-based Clustering Tool for Effective Spreadsheet Defect Detection 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 | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | FPChecker: Detecting Floating-Point Exceptions in GPU Applications Ignacio LagunaLawrence Livermore National Laboratory | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | PMExec: An Execution Engine of Partial UML-RT Models Mojtaba BagherzadehQueen's University, Karim JahedQueen's University, Nafiseh KahaniQueen's University, Juergen DingelQueen's University, Kingston, Ontario Pre-print |
Wed 13 Nov
13:40 - 15:20: Papers - Verification and Bug Detection at Cortez 1 Chair(s): Raghavan KomondoorIndian Institute of Science, Bangalore | ||||||||||||||||||||||||||||||||||||||||||
13:40 - 14:00 Talk | Mutation Analysis for Coq 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 - 14:20 Talk | Verifying Arithmetic in Cryptographic C Programs Jiaxiang LiuShenzhen University, Xiaomu ShiShenzhen University, Ming-Hsien TsaiAcademia Sinica, Taiwan, Bow-Yaw WangAcademia Sinica, Bo-Yin YangAcademia Sinica Pre-print | |||||||||||||||||||||||||||||||||||||||||
14:20 - 14:40 Talk | Model checking embedded control software using OS-in-the-loop CEGAR Pre-print | |||||||||||||||||||||||||||||||||||||||||
14:40 - 15:00 Talk | Get rid of inline assembly through verification-oriented lifting Frédéric RecoulesCEA LIST, Sebastien BardinCEA LIST, Richard BonichonCEA LIST, Laurent MounierUniversité Grenoble Alpes, Marie-Laure PotetUniversité Grenoble Alpes DOI Pre-print | |||||||||||||||||||||||||||||||||||||||||
15:00 - 15:10 Demonstration | VeriAbs : Verification by Abstraction and Test Generation 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 - 15:20 Demonstration | SGUARD: A Feature-based Clustering Tool for Effective Spreadsheet Defect Detection 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 |