ISSTA/ECOOP 2024
Mon 16 - Fri 20 September 2024 Vienna, Austria
Wed 18 Sep 2024 14:08 - 14:21 at EI 5 Hochenegg - Tool Demos 1 Chair(s): Rohan Padhye

This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pipeline. It transforms an input program into an abstract syntax tree to infer and add type information. Then, it translates Python expressions and statements into an intermediate representation. Finally, it converts this description into formulae evaluated with satisfiability modulo theories (SMT) solvers. The proposed approach was realized with the efficient SMT-based bounded model checker (ESBMC), which resulted in a tool called ESBMC-Python, the first BMC-based Python-code verifier. Experimental results, with a test suite specifically developed for this purpose, showed its effectiveness, where successful and failed tests were correctly evaluated. Moreover, it found a real problem in the Ethereum Consensus Specification.

Wed 18 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
Tool Demos 1Tool Demonstrations at EI 5 Hochenegg
Chair(s): Rohan Padhye Carnegie Mellon University
13:30
12m
Talk
Generalized Concurrency Testing Tool for Distributed Systems
Tool Demonstrations
Ege Berkay Gulcan Delft University of Technology, João Neto Delft University of Technology, Burcu Kulahcioglu Ozkan Delft University of Technology
DOI Media Attached
13:42
12m
Talk
Testing concurrent algorithms on JVM with Lincheck and IntelliJ IDEADistinguished Tool Demo Award
Tool Demonstrations
Alexander Potapov JetBrains, Maksim Zuev JetBrains, Evgenii Moiseenko JetBrains Research, Nikita Koval JetBrains
13:55
12m
Talk
JCWIT: A Correctness-Witness Validator for Java Programs based on Bounded Model Checking
Tool Demonstrations
Zaiyu Cheng University of Manchester, Tong Wu University of Manchester, Peter Schrammel University of Sussex and Diffblue Ltd, Norbert Tihanyi Eotvos Lorand University, Eddie B. de Lima Filho TPV Technology, Lucas C. Cordeiro University of Manchester, UK and Federal University of Amazonas, Brazil
14:08
12m
Talk
ESBMC-Python: A Bounded Model Checker for Python Programs
Tool Demonstrations
Bruno Farias University of Manchester, Rafael Menezes University of Manchester, Eddie B. de Lima Filho TPV Technology, Youcheng Sun University of Manchester, Lucas C. Cordeiro University of Manchester, UK and Federal University of Amazonas, Brazil
Media Attached
14:21
12m
Talk
Panda: A Concurrent Scheduler for Compiler-Based Tools
Tool Demonstrations
Xutong Ma Institute of Software, Chinese Academy of Sciences, Beijing, China, Jiwei Yan Institute of Software at Chinese Academy of Sciences, Jun Yan Institute of Software, Chinese Academy of Sciences, Jian Zhang Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
DOI Pre-print Media Attached
14:34
12m
Talk
SeeWasm: An Efficient and Fully-Functional Symbolic Execution Engine for WebAssembly Binaries
Tool Demonstrations
Ningyu He Peking University, Zhehao Zhao Peking University, Hanqin Guan Peking University, Jikai Wang Huazhong University of Science and Technology, Shreya Mathews IMC University of Applied Sciences Krems, Ding Li Peking University, Haoyu Wang Huazhong University of Science and Technology, Xiangqun Chen Peking University, Yao Guo Peking University
14:47
12m
Talk
PolyTracker: Whole-Input Dynamic Information Flow TracingDistinguished Tool Demo Award
Tool Demonstrations
Evan Sultanik Trail of Bits, Marek Surovič Trail of Bits, Henrik Brodin Trail of Bits, Kelly Kaoudis Trail of Bits, Facundo Tuesca Trail of Bits, Carson Harmon Trail of Bits, Lisa Overall Trail of Bits, Joseph Sweeney Trail of Bits, Bradford Larsen Trail of Bits

Information for Participants
Wed 18 Sep 2024 13:30 - 15:00 at EI 5 Hochenegg - Tool Demos 1 Chair(s): Rohan Padhye
Info for room EI 5 Hochenegg:

Map: https://tuw-maps.tuwien.ac.at/?q=CF0229

Room tech: https://raumkatalog.tiss.tuwien.ac.at/room/15705