Bounded Verification of Software Models: Challenges and Opportunities

Ensuring the absence of bugs in a software system is an important but very challenging problem. Early error detection within the development process reduces the cost of finding and fixing defects. Thus, the analysis of software models can improve its final quality and reduce its development costs. A promising research direction in this field is the use of boolean satisfiability (SAT) or constraint programming (CP) solvers to perform bounded verification. Bounded verification consists in formally checking the absence of errors within a finite space defined as a parameter of the analysis. This type of analysis is usually fast in practice and provides informative feedback. However, it is computationally complex in general and lacks conclusive results outside the verification bounds provided as parameters. In this paper, we discuss recent trends and results in the application of bounded verification to a specific field within software engineering: the analysis of models of a software system. Furthermore, we will discuss promising contributions that can build upon previous work to improve its applicability in practice within the software industry.