Affiner les résultats

Using linear algebra in decomposition of Farkas interpolants

Blicha, Martin ; Hyvärinen, Antti E. J. ; Kofroň, Jan ; Sharygina, Natasha

In: International journal on software tools for technology transfer, 2021, p. 15

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 ...

Decision Procedures for Flat Array Properties

Alberti, Francesco ; Ghilardi, Silvio ; Sharygina, Natasha

In: Journal of Automated Reasoning, 2015, vol. 54, no. 4, p. 327-352

An extension of lazy abstraction with interpolation for programs with arrays

Alberti, Francesco ; Bruttomesso, Roberto ; Ghilardi, Silvio ; Ranise, Silvio ; Sharygina, Natasha

In: Formal Methods in System Design, 2014, vol. 45, no. 1, p. 63-109

Resolution proof transformation for compression and interpolation

Rollini, Simone ; Bruttomesso, Roberto ; Sharygina, Natasha ; Tsitovich, Aliaksei

In: Formal Methods in System Design, 2014, vol. 45, no. 1, p. 1-41

An abstraction refinement approach combining precise and approximated techniques

Sharygina, Natasha ; Tonetta, Stefano ; Tsitovich, Aliaksei

In: International Journal on Software Tools for Technology Transfer, 2012, vol. 14, no. 1, p. 1-14

Loop summarization using state and transition invariants

Kroening, Daniel ; Sharygina, Natasha ; Tonetta, Stefano ; Tsitovich, Aliaksei ; Wintersteiger, Christoph

In: Formal Methods in System Design, 2013, vol. 42, no. 3, p. 221-261