@conference {319, title = {Accurate Smart Contract Verification through Direct Modelling}, booktitle = {ISoLA 2020 - 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation}, year = {2020}, publisher = {Springer International Publishing}, organization = {Springer International Publishing}, isbn = {978-3-030-61467-6}, doi = {doi.org/10.1007/978-3-030-61467-6_12}, url = {https://link.springer.com/chapter/10.1007\%2F978-3-030-61467-6_12}, author = {Matteo Marescotti and Rodrigo Otoni and Leonardo Alt and Patrick Eugster and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {227, title = {Automated Discovery of Simulation Between Programs}, booktitle = {LPAR}, year = {2015}, author = {Grigory Fedyukovich and Gurfinkel, A. and Natasha Sharygina} } @article {173, title = {Abstraction and Acceleration in SMT-based Model-Checking for Array Programs}, journal = {CoRR}, volume = {April 2013}, year = {2013}, author = {Francesco Alberti and Ghilardi, S. and Natasha Sharygina} } @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} } @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 {157, title = {Automated Verification of Security Policies in Mobile Code.}, booktitle = {Integrated Formal Methods (IFM)}, year = {2007}, publisher = {Springer, Volume 4591}, organization = {Springer, Volume 4591}, abstract = {

This paper describes an approach for the automated verification of mobile programs. Mobile systems are characterized by the explicit notion of locations (e.g., sites where they run) and the ability to execute at different locations, yielding a number of security issues. We give formal semantics to mobile systems as Labeled Kripke Structures, which encapsulate the notion of the location net. The location net summarizes the hierarchical nesting of threads constituting a mobile program and enables specifying security policies. We formalize a language for specifying security policies and show how mobile programs can be exhaustively analyzed against any given security policy by using model checking techniques.
We developed and experimented with a prototype framework for analysis of mobile code, using the SATABS model checker. Our approach relies on SATABS{\textquoteright}s support for unbounded thread creation and enhances it with location net abstractions, which are essential for verifying large mobile programs. Our experimental results on various benchmarks are encouraging and demonstrate advantages of the model checking-based approach, which combines the validation of security properties with other checks, such as for buffer overflows.

}, author = {Braghin, C. and Natasha Sharygina and Katerina Barone Adesi} }