Failure-Directed Program Trimming (Extended Version)
Kostas Ferles, Valentin W\"ustholz, Maria Christakis, Isil Dillig

TL;DR
This paper introduces program trimming, a technique that simplifies programs by reducing execution paths while preserving safety properties, thereby enhancing the scalability and effectiveness of safety checking tools.
Contribution
It presents a novel program trimming method and a lightweight static analysis for equi-safety reduction, implemented in the Trimmer tool, improving safety analysis techniques.
Findings
Significantly improves abstract interpretation and symbolic execution effectiveness.
Reduces program paths without losing safety guarantees.
Enhances scalability of safety checking tools.
Abstract
This paper describes a new program simplification technique called program trimming that aims to improve the scalability and precision of safety checking tools. Given a program , program trimming generates a new program such that and are equi-safe (i.e., has a bug if and only if has a bug), but has fewer execution paths than . Since many program analyzers are sensitive to the number of execution paths, program trimming has the potential to improve the effectiveness of safety checking tools. In addition to introducing the concept of program trimming, this paper also presents a lightweight static analysis that can be used as a pre-processing step to remove program paths while retaining equi-safety. We have implemented the proposed technique in a tool called Trimmer…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Testing and Debugging Techniques · Software Reliability and Analysis Research · Software Engineering Research
