Write a Blog >>
ICST 2022
Mon 4 - Fri 8 April 2022
Thu 7 Apr 2022 17:00 - 17:15 at Margaret Hamilton - ICST Symbolic execution Chair(s): Arie van Deursen

In the last three decades, memory safety issues in system programming languages such as C or C++ have been one of the most significant sources of security vulnerabilities. However, there exist only a few attempts with limited success to cope with the complexity of C++ program verification. We describe and evaluate a novel verification approach based on bounded model checking (BMC) and satisfiability modulo theories (SMT) to verify C++ programs. Our verification approach analyses bounded C++ programs by encoding into SMT various sophisticated features that the C++ programming language offers, such as templates, inheritance, polymorphism, exception handling, and the Standard Template Libraries. We formalize these features within our formal verification framework using a decidable fragment of first-order logic and then show how state-of-the-art SMT solvers can efficiently handle that. We implemented our verification approach on top of ESBMC. We compare ESBMC to LLBMC and DIVINE, which are state-of-the-art verifiers to check C++ programs directly from the LLVM bitcode. Experimental results show that ESBMC can handle a wide range of C++ programs, presenting a higher number of correct verification results. Additionally, ESBMC has been applied to a commercial C++ application in the telecommunication domain and successfully detected arithmetic-overflow errors, which could potentially lead to security vulnerabilities.

Thu 7 Apr

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

16:45 - 18:00
ICST Symbolic executionResearch Papers / Industry / Testing Tools / Journal-First Papers at Margaret Hamilton
Chair(s): Arie van Deursen Delft University of Technology, Netherlands
Translating EULYNX SysML models into Symbolic Transition Systems for Model-Based Testing of Railway signaling systems
Tobias Bachmann Universiteit van Amsterdam, Machiel van der Bijl Axini, Daan van der Meij ProRail, Djurre van der Wal University of Twente, Ana Maria Oprescu University of Amsterdam
Model checking C++ programs
Journal-First Papers
Felipe R. Monteiro Amazon, Mikhail R. Gadelha Igalia, Lucas C. Cordeiro University of Manchester, UK
Link to publication DOI
SIFT: A Tool for Property Directed Symbolic Execution of Multithreaded Software
Testing Tools
Tuba Yavuz University of Florida
Automating Differential Testing with Overapproximate Symbolic Execution
Research Papers
Richard Rutledge Georgia Institute of Technology, Alessandro Orso Georgia Tech
Live Q&A
Discussion and Q&A
Research Papers