ASE 2022 (series) / Tool Demonstrations /
CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory
Wed 12 Oct 2022 09:30 - 10:00 at Ballroom A - Tool Poster Session 2
Thu 13 Oct 2022 16:00 - 16:10 at Banquet B - Technical Session 32 - Formal Methods and Models II Chair(s): Khouloud Gaaloul
Thu 13 Oct 2022 16:00 - 16:10 at Banquet B - Technical Session 32 - Formal Methods and Models II Chair(s): Khouloud Gaaloul
Dynamic program analysis tools such as Eraser, Memcheck, or ThreadSanitizer abstract the contents of individual memory locations and store the abstraction results in a separate data structure called shadow memory. They then use this meta-information to efficiently implement the actual analyses. In this paper, we describe the implementation of an efficient symbolic shadow memory extension for the CBMC bounded model checker that can be accessed through an API, and sketch its use in the design of a new data race analyzer that is implemented by a code-to-code translation. Artifact/tool URL: shorturl.at/jzVZ0 Video URL: youtu.be/pqlbyiY5BLU
Wed 12 OctDisplayed time zone: Eastern Time (US & Canada) change
Wed 12 Oct
Displayed time zone: Eastern Time (US & Canada) change
09:30 - 10:00 | |||
09:30 30mDemonstration | ElecDaug: Electromagnetic Data Augmentation for Model Repair based on Metamorphic Relation Tool Demonstrations Jiawei He , Zhida Bao Harbin Engineering University, Quanjun Zhang Nanjing University, Weisong Sun State Key Laboratory for Novel Software Technology, Nanjing University, Jiawei Liu Nanjing University, Chunrong Fang Nanjing University, Yun Lin National University of Singapore | ||
09:30 30mDemonstration | CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory Tool Demonstrations Bernd Fischer Stellenbosch University, South Africa, Salvatore La Torre Università degli Studi di Salerno, Gennaro Parlato University of Molise, Peter Schrammel University of Sussex and Diffblue Ltd | ||
09:30 30mDemonstration | ADEPT: A Testing Platform for Simulated Autonomous DrivingVirtual Tool Demonstrations Sen Wang Nanjing University, Zhuheng Sheng Nanjing University, Jingwei Xu , Taolue Chen University of Surrey, UK, Junjun Zhu Nanjing University, Shuhui Zhang Nanjing University, Yuan Yao Nanjing University, Xiaoxing Ma Nanjing University | ||
09:30 30mDemonstration | Augur: Dynamic Taint Analysis for Asynchronous JavaScript Tool Demonstrations Mark W. Aldrich Tufts University, Alexi Turcotte Northeastern University, Matthew Blanco Northeastern University, Frank Tip Northeastern University | ||
09:30 30mDemonstration | FlexType: A Plug-and-Play Framework for Type Inference Models Tool Demonstrations Sivani Voruganti UC Davis, Kevin Jesse University of California at Davis, USA, Prem Devanbu Department of Computer Science, University of California, Davis Pre-print | ||
09:30 30mDemonstration | InvCon: A Dynamic Invariant Detector for Ethereum Smart Contracts Tool Demonstrations Pre-print | ||
09:30 30mDemonstration | AntiCopyPaster: Extracting Code Duplicates As Soon As They Are Introduced in the IDE Tool Demonstrations Eman Abdullah AlOmar Stevens Institute of Technology, Anton Ivanov HSE University, Zarina Kurbatova JetBrains Research, Yaroslav Golubev JetBrains Research, Mohamed Wiem Mkaouer Rochester Institute of Technology, Ali Ouni ETS Montreal, University of Quebec, Timofey Bryksin JetBrains Research, Le Nguyen Rochester Institute of Technology, Amit Kini Rochester Institute of Technology, Aditya Thakur Rochester Institute of Technology DOI Pre-print | ||
09:30 30mDemonstration | ecoCode: a SonarQube Plugin to Remove Energy Smells from Android Projects Tool Demonstrations DOI File Attached | ||
09:30 30mDemonstration | Answering Software Deployment Questions via Neural Machine Reading at ScaleVirtual Tool Demonstrations Guan Jie Qiu School of Software, Shanghai Jiao Tong University, Diwei Chen School of Software, Shanghai Jiao Tong University, Shuai Zhang School of Software, Shanghai Jiao Tong University, Yitian Chai School of Software, Shanghai Jiao Tong University, Xiaodong Gu Shanghai Jiao Tong University, China, Beijun Shen School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University | ||
09:30 30mDemonstration | LiveRef: a Tool for Live Refactoring Java Code Tool Demonstrations Sara Fernandes FEUP, Universidade do Porto, Ademar Aguiar FEUP, Universidade do Porto, André Restivo LIACC, Universidade do Porto, Porto, Portugal | ||
09:30 30mDemonstration | A transformer-based IDE plugin for vulnerability detectionVirtual Tool Demonstrations Cláudia Mamede FEUP, U.Porto, Eduard Pinconschi FEUP, U.Porto, Rui Abreu Faculty of Engineering, University of Porto, Portugal | ||
Thu 13 OctDisplayed time zone: Eastern Time (US & Canada) change
Thu 13 Oct
Displayed time zone: Eastern Time (US & Canada) change
16:00 - 18:00 | Technical Session 32 - Formal Methods and Models IITool Demonstrations / Journal-first Papers / Research Papers at Banquet B Chair(s): Khouloud Gaaloul University of Michigan - Dearborn | ||
16:00 10mDemonstration | CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory Tool Demonstrations Bernd Fischer Stellenbosch University, South Africa, Salvatore La Torre Università degli Studi di Salerno, Gennaro Parlato University of Molise, Peter Schrammel University of Sussex and Diffblue Ltd | ||
16:10 20mResearch paper | Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses Research Papers Elias Kuiter Otto-von-Guericke-University Magdeburg, Sebastian Krieter University of Ulm, Chico Sundermann University of Ulm, Thomas Thüm University of Ulm, Gunter Saake University of Magdeburg, Germany | ||
16:30 20mPaper | A three-valued model abstraction framework for PCTL* stochastic model checkingVirtual Journal-first Papers Yang Liu Shanghai Maritime University/National University of Singapore, Yan Ma Nanjing University of Finance and Economics / National University of Singapore, Yongsheng Yang Shanghai Maritime University File Attached | ||
16:50 20mResearch paper | Finding and Understanding Incompleteness Bugs in SMT SolversVirtual Research Papers | ||
17:10 20mResearch paper | Checking LTL Satisfiability via End-to-end LearningVirtual Research Papers Weilin Luo School of Computer Science and Engineering, Sun Yat-sen University, Hai Wan School of Data and Computer Science, Sun Yat-sen University, Delong Zhang SUN YAT-SEN UNIVERSITY, Jianfeng Du Guangdong University of Foreign Studies, Hengdi Su SUN YAT-SEN UNIVERSITY | ||
17:30 20mResearch paper | QVIP: An ILP-based Formal Verification Approach for Quantized Neural NetworksVirtual Research Papers Yedi Zhang ShanghaiTech University, Zhe Zhao ShanghaiTech University, Guangke Chen ShanghaiTech University, Fu Song ShanghaiTech University, Min Zhang East China Normal University, Taolue Chen Birkbeck University of London, Jun Sun Singapore Management University | ||