@conference {375, title = {Symbolic Model Checking for TLA+ Made Faster}, booktitle = {TACAS - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, year = {2023}, address = {Paris}, url = {https://doi.org/10.1007/978-3-031-30823-9_7}, author = {Rodrigo Otoni and Igor Konnov and Jure Kukovec and Patrick Eugster and Natasha Sharygina} } @article {356, title = {Using linear algebra in decomposition of Farkas interpolants}, journal = {International Journal on Software Tools for Technology Transfer}, year = {2021}, type = {Journal}, abstract = {

The use of propositional logic and systems of linear inequalities over reals is a common means to model software for formal verification. Craig interpolants constitute a central building block in this setting for over-approximating reachable states, e.g. as candidates for inductive loop invariants. Interpolants for a linear system can be efficiently computed from a Simplex refutation by applying the Farkas{\textquoteright} lemma. However, these interpolants do not always suit the verification task{\textemdash}in the worst case, they can even prevent the verification algorithm from converging. This work introduces the decomposed interpolants, a fundamental extension of the Farkas interpolants, obtained by identifying and separating independent components from the interpolant structure, using methods from linear algebra. We also present an efficient polynomial algorithm to compute decomposed interpolants and analyse its properties. We experimentally show that the use of decomposed interpolants in model checking results in immediate convergence on instances where state-of-the-art approaches diverge. Moreover, since being based on the efficient Simplex method, the approach is very competitive in general.

}, url = {https://link.springer.com/article/10.1007/s10009-021-00641-z}, author = {Martin Blicha and Antti E. J. Hyv{\"a}rinen and Jan Kofron and Natasha Sharygina} } @conference {298, title = {Decomposing Farkas Interpolants}, booktitle = {TACAS}, year = {2019}, author = {Martin Blicha and Antti E. J. Hyv{\"a}rinen and Jan Kofron and Natasha Sharygina} } @article {351, title = {Exploiting partial variable assignment in interpolation-based model checking.}, journal = {Formal Methods in System Design}, year = {2019}, abstract = {

Craig interpolation has been successfully employed in symbolic program verification as a means of abstraction for sets of program states. In this article, we present the partial variable assignment interpolation system, an extension of the labeled interpolation system, enriched by partial variable assignments. It allows for both generation of smaller interpolants as well as for their faster computation. We present proofs of important properties of the interpolation system as well as a set of experiments proving its usefulness.

}, url = {https://link.springer.com/article/10.1007\%2Fs10703-019-00342-z}, author = {Pavel Jan{\v c}{\'\i}k and Jan Kofron and Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {234, title = {PVAIR: Partial Variable Assignment InterpolatoR}, booktitle = {FASE2016}, year = {2016}, url = {http://verify.inf.usi.ch/sites/default/files/main-2.pdf}, author = {Pavel Jan{\v c}{\'\i}k and Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Jan Kofron and Natasha Sharygina} } @conference {210, title = {On Interpolants and Variable Assignments}, booktitle = {Formal Methods in Computer-Aided Design (FMCAD)}, year = {2014}, address = {Lausanne, Switzerland}, author = {Jancik, P. and KofronĖ‡, J. and Rollini, S.F. and Natasha Sharygina} } @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.} } @conference {160, title = {A Parametric Interpolation Framework for First-Order Theories}, booktitle = {12th Mexican International Conference on Artificial Intelligence (MICAI)}, year = {2013}, author = {Kovacs, L. and Rollini, S.F. and Natasha Sharygina} } @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} } @conference {154, title = {Termination Analysis with Compositional Transition Invariants}, booktitle = {International Conference on Computer-Aided Verification (CAV)}, year = {2010}, publisher = {Springer}, organization = {Springer}, address = {Edinburgh, UK}, abstract = {

Modern termination provers rely on a safety checker to construct disjunctively well-founded transition invariants. This safety check\ is known to be the bottleneck of the procedure. We present an alternative algorithm that uses a light-weight check based on transitivity of\ ranking relations to prove program termination. We provide an experimental evaluation over a set of 87 Windows drivers, and demonstrate\ that our algorithm is often able to conclude termination by examining\ only a small fraction of the program. As a consequence, our algorithm is\ able to outperform known approaches by multiple orders of magnitude.\ 

}, author = {Kroening, D. and Natasha Sharygina and Tsitovich, A. and Wintersteiger, C.M.} } @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 {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.} }