Control flow graph, formal verification and constraint programming techniques

Jesse Deveza, Lanier Santos, Rosiane de Freitas, Lucas Cordeiro

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Formal program verification is a generally undecidable problem. Bounded Model Checking (BMC) is one method that can achieve decidability by searching for violations of properties of a program up to a bound k. BMC reduces the program verification problem to the classic NP-complete Boolean Satisfiability (SAT). However, it can still lead to an exponential state-space exploration due to the program’s large and possibly unbounded loops. In this case, there might be many execution paths to traverse through a program during its symbolic execution. Therefore, the control flow or computation during the program’s execution, mainly in symbolic execution, can be represented as a directed graph named Control Flow Graph (CFG). In this work, we present the properties of the CFG and discuss the application of constraint programming techniques to reduce variable domains as a preprocessing step or during the BMC process for verifying software systems. We also describe how constraint programming can be exploited to prove the (partial) correctness of the program via proof by induction built on top of BMC.
Original languageEnglish
Title of host publication10th Latin American Workshop on Cliques in Graphs (LAWCG)
Publication statusAccepted/In press - 15 Jun 2022

Fingerprint

Dive into the research topics of 'Control flow graph, formal verification and constraint programming techniques'. Together they form a unique fingerprint.

Cite this