Abstract
In software verification, scope-bounded checking of programs has become an effective technique for finding subtle bugs. Given bounds (that are iteratively relaxed) on input size and length of execution paths, a program and its correctness specifications are translated into a formula, which is solved using off-the-shelf solvers – a solution to the formula is a counterexample to the correctness specification.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Dennis, G., Chang, F.S.H., Jackson, D.: Modular verification of code with SAT. In: ISSTA (2006)
Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA (2000)
Shao, D., Khurshid, S., Perry, D.E.: An incremental approach to scope-bounded checking using a lightweight formal method. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009: Formal Methods. LNCS, vol. 5850, pp. 757–772. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shao, D., Gopinath, D., Khurshid, S., Perry, D.E. (2010). A Case for Using Data-Flow Analysis to Optimize Incremental Scope-Bounded Checking. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds) Abstract State Machines, Alloy, B and Z. ABZ 2010. Lecture Notes in Computer Science, vol 5977. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11811-1_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-11811-1_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11810-4
Online ISBN: 978-3-642-11811-1
eBook Packages: Computer ScienceComputer Science (R0)