Lattice-Based Refinement in Bounded Model Checking
VSTTE, pp. 50-68, 2018.
In this paper we present an algorithm for bounded model-checking with SMT solvers of programs with library functions—either standard or user-defined. Typically, if the program correctness depends on the output of a library function, the model-checking process either treats this function as an uninterpreted function, or is required to use ...More
Full Text (Upload PDF)
PPT (Upload PPT)