ASE 2019 (series) / Demonstrations /
VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-Threaded Programs with Lazy-CSeq
Wed 13 Nov 2019 10:00 - 10:40 at Kensington Ballroom - Poster Session: Tool Demonstrations 2
Thu 14 Nov 2019 12:00 - 12:10 at Cortez 1 - Concurrency Chair(s): Elena Sherman
Thu 14 Nov 2019 12:00 - 12:10 at Cortez 1 - Concurrency Chair(s): Elena Sherman
Swarm-based verification methods split a verification problem into a large number of independent simpler tasks and so exploit the availability of large numbers of cores to speed up verification. Lazy-CSeq is a BMC-based bug-finding tool for C programs using POSIX threads that is based on sequentialization. Here we present the tool VeriSmart 2.0, which extends Lazy-CSeq with a swarm-based bug-finding method. The key idea of this approach is to constrain the interleavings such that context switches can only happen within selected tiles (more specifically, contiguous code segments within the individual threads). This under-approximates the program’s behaviors, with the number and size of tiles as additional parameters, which allows us to vary the complexity of the tasks. Overall, this significantly improves peak memory consumption and (wall-clock) analysis time.
Wed 13 NovDisplayed time zone: Tijuana, Baja California change
Wed 13 Nov
Displayed time zone: Tijuana, Baja California change
10:00 - 10:40 | |||
10:00 40mDemonstration | TsmartGP: A Tool for Finding Memory Defects with Pointer Analysis Demonstrations Yuexing Wang Tsinghua University, Guang Chen Tsinghua University, Min Zhou Tsinghua University, Ming Gu Tsinghua University, Jiaguang Sun Tsinghua University | ||
10:00 40mDemonstration | BuRRiTo: A Framework to Extract, Specify, Verify and Analyze Business Rules Demonstrations Pavan Kumar Chittimalli TCS Research, Kritika Anand TCS Research, Shrishti Pradhan TCS Research, Sayandeep Mitra TCS Research, Chandan Prakash TCS Research, Rohit Shere TCS Research, Ravindra Naik TCS Research, TRDDC, India | ||
10:00 40mDemonstration | Lancer: Your Code Tell Me What You Need Demonstrations Shufan Zhou School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Beijun Shen School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Hao Zhong Shanghai Jiao Tong University | ||
10:00 40mDemonstration | TestCov: Robust Test-Suite Execution and Coverage Measurement Demonstrations Pre-print Media Attached File Attached | ||
10:00 40mDemonstration | Prema: A Tool for Precise Requirements Editing, Modeling and Analysis Demonstrations Yihao Huang East China Normal University, Jincao Feng East China Normal University, Hanyue Zheng East China Normal University, Jiayi Zhu East China Normal University, Shang Wang East China Normal University, Siyuan Jiang Eastern Michigan University, Weikai Miao Shanghai Key Lab for Trustworthy Computing, School of Computer Science and Software Engineering, East China Normal University, Geguang Pu East China Normal University&Shanghai Trusted Industrial Control Platform Co., Ltd | ||
10:00 40mDemonstration | XRaSE: Towards Virtually Tangible Software using Augmented Reality Demonstrations Rohit Mehra Accenture Labs, India, Vibhu Saujanya Sharma Accenture Labs, Vikrant Kaulgud Accenture Labs, India, Sanjay Podder Accenture | ||
10:00 40mDemonstration | MuSC: A Tool for Mutation Testing of Ethereum Smart Contract Demonstrations Zixin Li Nanjing University, Haoran Wu State Key Laboratory for Novel Software Technology, Nanjing University, Jiehui Xu Nanjing University, Xingya Wang State Key Laboratory for Novel Software Technology, Nanjing University, Lingming Zhang The University of Texas at Dallas, Zhenyu Chen Nanjing University | ||
10:00 40mDemonstration | VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-Threaded Programs with Lazy-CSeq Demonstrations Bernd Fischer Stellenbosch University, Salvatore La Torre Università degli Studi di Salerno, Gennaro Parlato University of Molise | ||
10:00 40mDemonstration | DeepMutation++: a Mutation Testing Framework for Deep Learning Systems Demonstrations Qiang Hu Kyushu University, Japan, Lei Ma Kyushu University, Xiaofei Xie Nanyang Technological University, Bing Yu Kyushu University, Japan, Yang Liu Nanyang Technological University, Singapore, Jianjun Zhao Kyushu University | ||
10:00 40mDemonstration | Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts Demonstrations Mark Mossberg Trail of Bits, Felipe Manzano Trail of Bits, Eric Hennenfent Trail of Bits, Alex Groce Northern Arizona University, Gustavo Grieco Trail of Bits, Josselin Feist Trail of Bits, Trent Brunson Trail of Bits, Artem Dinaburg Trail of Bits Media Attached | ||
10:00 40mDemonstration | ConVul: An Effective Tool for Detecting Concurrency Vulnerabilities Demonstrations Ruijie Meng University of Chinese Academy of Sciences, Biyun Zhu University of Chinese Academy of Sciences, Hao Yun University of Chinese Academy of Sciences, Haicheng Li University of Chinese Academy of Sciences, Yan Cai Institute of Software, Chinese Academy of Sciences, Zijiang Yang Western Michigan University | ||
10:00 40mDemonstration | mCUTE: A Model-level Concolic Unit Testing Engine for UML State Machines Demonstrations Reza Ahmadi Queen's University, Karim Jahed Queen's University, Juergen Dingel Queen's University, Kingston, Ontario | ||
Thu 14 NovDisplayed time zone: Tijuana, Baja California change
Thu 14 Nov
Displayed time zone: Tijuana, Baja California change
10:40 - 12:20 | ConcurrencyResearch Papers / Demonstrations at Cortez 1 Chair(s): Elena Sherman Boise State University | ||
10:40 20mTalk | MAP-Coverage: a Novel Coverage Criterion for Testing Thread-Safe Classes Research Papers Zan Wang College of Intelligence and Computing, Tianjin University, Yingquan Zhao Tianjin University, Shuang Liu College of Intelligence and Computing, Tianjin University, Jun Sun Singapore Management University, Singapore, Xiang Chen School of Information Science and Technology, Nantong University, Huarui Lin College of Intelligence and Computing, Tianjin University | ||
11:00 20mTalk | Automating Non-Blocking Synchronization In Concurrent Data Abstractions Research Papers Jiange Zhang University of Colorado Colorado Springs, Qing Yi University of Colorado Colorado Springs, Damian Dechev University of Central Florida Pre-print | ||
11:20 20mTalk | Automating CUDA Synchronization via Program Transformation Research Papers Mingyuan Wu Southern University of Science and Technology, Lingming Zhang The University of Texas at Dallas, Cong Liu Eindhoven University of Technology, Shin Hwei Tan , Yuqun Zhang Southern University of Science and Technology | ||
11:40 20mTalk | Efficient Transaction-Based Deterministic Replay for Multi-threaded Programs Research Papers Ernest Bota Pobee City University of Hong Kong, Xiupei Mei City University of Hong Kong, Wing-Kwong Chan City University of Hong Kong, Hong Kong | ||
12:00 10mDemonstration | VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-Threaded Programs with Lazy-CSeq Demonstrations Bernd Fischer Stellenbosch University, Salvatore La Torre Università degli Studi di Salerno, Gennaro Parlato University of Molise | ||
12:10 10mDemonstration | ConVul: An Effective Tool for Detecting Concurrency Vulnerabilities Demonstrations Ruijie Meng University of Chinese Academy of Sciences, Biyun Zhu University of Chinese Academy of Sciences, Hao Yun University of Chinese Academy of Sciences, Haicheng Li University of Chinese Academy of Sciences, Yan Cai Institute of Software, Chinese Academy of Sciences, Zijiang Yang Western Michigan University | ||