@article {340, title = {An abstraction refinement approach combining precise and approximated techniques}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {14}, year = {2012}, 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 a given set of predicates. A precise abstraction contains the minimal set of transitions with regard to the predicates, 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 approach that employs both precise (slow) and approximated (fast) abstraction techniques within one abstraction-refinement loop. 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 almost systematically outperforms both precise and imprecise techniques.

}, url = {https://link.springer.com/article/10.1007/s10009-011-0185-y}, author = {Natasha Sharygina and Stefano Tonetta and Aliaksei Tsitovich} } @conference { twks11, title = {Loop Summarization and Termination Analysis}, booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, volume = {6605}, year = {2011}, pages = {81-95}, publisher = {Springer}, organization = {Springer}, address = {Saarbr{\"u} Germany}, url = {http://dx.doi.org/10.1007/978-3-642-19835-9_9}, author = {Aliaksei Tsitovich and Natasha Sharygina and Christoph M. Wintersteiger and Kroening, Daniel} } @mastersthesis { Aliaksei Tsitovi, title = {Scalable Abstractions for Efficient Security Checks}, year = {2011}, pages = {164}, school = {University of Lugano}, type = {PhD Thesis}, address = {Lugano}, author = {Aliaksei Tsitovich} }