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
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)