@article {164, title = {Loop summarization using state and transition invariants}, journal = {Formal Methods in System Design}, volume = {42}, year = {2013}, issn = {0925-9856}, author = {Kroening, D. and Natasha Sharygina and Tonetta, S. and Tsitovich, A. and Wintersteiger, C.M.} } @article { Natasha Sharygin, title = {An abstraction refinement approach combining precise and approximated techniques}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {14}, year = {2012}, pages = {1-14}, publisher = {Springer}, keywords = {Approximated abstraction, CEGAR, Precise abstraction, Predicate abstraction}, url = {http://dx.doi.org/10.1007/s10009-011-0185-y}, author = {Natasha Sharygina and Tonetta, S. and Tsitovich, A.} } @conference {153, title = {Loopfrog: A Static Analyzer for ANSI-C Programs}, booktitle = {The 24th IEEE/ACM International Conference on Automated Software Engineering}, year = {2009}, publisher = {IEEE Computer Society}, organization = {IEEE Computer Society}, address = {Auckland, New Zealand}, abstract = {

Practical software verification is dominated by two major classes of techniques. The first is model checking, which provides total precision, but suffers from the state space explosion problem. The second is abstract interpretation, which is usually much less demanding, but often returns a high number of false positives.

We present Loopfrog, a static analyzer that combines the best of both worlds: the precision of model checking and the performance of abstract interpretation. In contrast to traditional static analyzers, it also provides "leaping" counterexamples to aid in the diagnosis of errors.

}, author = {Kroening, D. and Natasha Sharygina and Tonetta, S. and Tsitovich, A. and Wintersteiger, C.M.} } @conference {156, title = {The Synergy of Precise and Fast Abstractions for Program Verification}, booktitle = {24th Annual ACM Symposium on Applied Computing (SAC)}, year = {2009}, publisher = {ACM}, organization = {ACM}, address = {Honolulu, USA}, abstract = {

Predicate abstraction is a powerful technique to reduce the state space of a program to a finite and affordable number of states. It produces a conservative over-approximation where concrete states are grouped together according to the predicates. Given a set of predicates, a precise abstraction contains the minimal set of transitions, but as a result is computationally expensive. Most model checkers therefore approximate the abstraction to alleviate the computation of the abstract system by trading off precision with cost. However, approximation results in a higher number of refinement iterations, since it can produce more false counterexamples than its precise counterpart. The refinement loop can become prohibitively expensive for large programs.

This paper proposes a new abstraction refinement technique that combines slow and precise predicate abstraction techniques with fast and imprecise ones. It allows computing the abstraction quickly, but keeps it precise enough to avoid too many refinement iterations. We implemented the new algorithm in a state-of-the-art software model checker. Our tests with various real life benchmarks show that the new approach systematically outperforms both precise and imprecise techniques.

}, author = {Natasha Sharygina and Tonetta, S. and Tsitovich, A.} } @conference {152, title = {Loop Summarization using Abstract Transformers}, booktitle = {6th International Symposium on Automated Technology for Verification and Analysis (ATVA)}, year = {2008}, publisher = {Springer, Volume 5311}, organization = {Springer, Volume 5311}, address = {Seoul, South Korea}, abstract = {

Existing program analysis tools that implement abstraction rely on saturating procedures to compute over-approximations of fixpoints. As an alternative, we propose a new algorithm to compute an over-approximation of the set of reachable states of a program by replacing loops in the control flow graph by their abstract transformer. Our technique is able to generate diagnostic information in case of property violations, which we call leaping counterexamples. We have implemented this technique and report experimental results on a set of large ANSI-C programs using abstract domains that focus on properties related to string-buffers.

}, author = {Kroening, D. and Natasha Sharygina and Tonetta, S. and Tsitovich, A. and Wintersteiger, C.M.} }