A Case for Using Data-Flow Analysis to Optimize Incremental Scope-Bounded Checking

Danhua Shao, Divya Gopinath, Sarfraz Khurshid, Dewayne E. Perry
Digital Printed Abstract View Cite
Type
Short Paper
Publication
2nd International Conference on ASM, Alloy, B, and Z (ABZ'10)

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{ShaoGKP10,
  author       = {Danhua Shao and
                  Divya Gopinath and
                  Sarfraz Khurshid and
                  Dewayne E. Perry},
  editor       = {Marc Frappier and
                  Uwe Gl{\"{a}}sser and
                  Sarfraz Khurshid and
                  R{\'{e}}gine Laleau and
                  Steve Reeves},
  title        = {A Case for Using Data-Flow Analysis to Optimize Incremental Scope-Bounded
                  Checking},
  booktitle    = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
                  {ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5977},
  pages        = {392--393},
  publisher    = {Springer},
  year         = {2010},
  url          = {https://doi.org/10.1007/978-3-642-11811-1\_30},
  doi          = {10.1007/978-3-642-11811-1\_30},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/ShaoGKP10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'10

Related