Program verification is an undecidable problem; all program verifiers must make a tradeoff between precision and scalability. Over the past decade, a variety of scalable program analysis tools have been developed. These tools, based primarily on techniques such as type systems and dataflow analysis, scale to large and realistic programs. However, to achieve scalability they sacrifice precision, resulting in a significant number of false error reports and adversely affecting the usability of the tool.
CITATION STYLE
Qadeer, S. (2009). Algorithmic Verification of Systems Software Using SMT Solvers (pp. 2–2). https://doi.org/10.1007/978-3-642-03237-0_2
Mendeley helps you to discover research relevant for your work.