BRICK: Path Enumeration Based Bounded Reachability Checking of C Program (Competition Contribution)
Lei Bu, Zhunyi Xie, Lecheng Lyu, Yichao Li, Xiao Guo, Jianhua Zhao, Xuandong Li
Abstract
Abstract BRICK is a bounded reachability checker for embedded C programs. BRICK conducts a path-oriented style checking of the bounded state space of the program, that enumerates and checks all the possible paths of the program in the threshold one by one. To alleviate the path explosion problem, BRICK locates and records unsatisfiable core path segments during the checking of each path and uses them to prune the search space. Furthermore, derivative free optimization based falsification and loop induction are introduced to handle complex program features like nonlinear path conditions and loops efficiently.
Topics & Concepts
ReachabilityBounded functionPath (computing)Computer scienceModel checkingState (computer science)State spaceAlgorithmMathematical optimizationTheoretical computer scienceMathematicsProgramming languageStatisticsMathematical analysisFormal Methods in VerificationSoftware Testing and Debugging TechniquesSoftware Reliability and Analysis Research