@conference {405, title = {Validation of CHC Satisfiability with ATHENA}, year = {2025}, abstract = {Formal veriication tooling increasingly relies on logic solvers as automated reasoning engines. A commonality among these solvers is the high complexity of their codebases, which makes bug occurrence disturbingly frequent. Tool competitions have showcased many examples of state-of-the-art solvers disagreeing on the satisiability of logic formulas, be it solvers for Boolean satisiability (SAT), satisiability modulo theories (SMT), or constrained Horn clauses (CHC). The validation of solvers{\textquoteright} results is thus of paramount importance, in order to increase the conidence not only in the solvers themselves, but also in the tooling which they underpin. Among the formalisms commonly used by modern veriication tools, CHC is one that has seen, at the same time, extensive practical usage and very little eforts in result validation. We propose a two-layered validation approach for witnesses of CHC satisiability that validates CHC models via proof-backed SMT queries. We developed a modular evaluation framework, ATHENA, and assessed the approach{\textquoteright}s viability via large scale experimentation, comparing three CHC solvers, ive SMT solvers, and ive proof checkers. Our results indicate that the approach is feasible, with potential to be incorporated into CHC-based tooling, and also conirm the need for validation, with fourteen bugs being found in the tools used.}, url = {https://dl.acm.org/doi/10.1145/3716505}, author = {Otoni Rodrigo and Blicha Martin and Eugster Patrick and Sharygina Natasha} } @conference {190, title = {Verification-Aided Regression Testing}, booktitle = {ISSTA}, year = {2014}, month = {06/2014}, abstract = {

In this paper we present Verification-Aided Regression Testing (VART), a novel extension of regression testing that uses model checking to increase the fault revealing capability of existing test suites. The key idea in VART is to extend the use of test case executions from the conventional direct fault discovery to the generation of behavioral properties specific to the upgrade, by (i) automatically producing properties that are proved to hold for the base version of a program, (ii) automatically identifying and checking on the upgraded program only the properties that, according to the developers{\textquoteright} intention, must be preserved by the upgrade, and (iii) reporting the faults and the corresponding counter-examples that are not revealed by the regression tests. Our empirical study on both open source and industrial software systems shows that VART automatically produces properties that increase the effectiveness of testing by automatically detecting faults unnoticed by the existing regression test suites.\ 

}, author = {Pastore, F. and Mariani, L. and Antti E. J. Hyv{\"a}rinen and Grigory Fedyukovich and Natasha Sharygina and Sehestedt, S. and Muhammad, A.} } @conference { BPS10, title = {A Flexible Schema for Generating Explanations in Lazy Theory Propagation}, booktitle = {International Conference on Formal Methods and Models for Codesign (MEMOCODE)}, year = {2010}, note = {to appear}, publisher = {IEEE Computer Society}, organization = {IEEE Computer Society}, address = {Grenoble, France}, author = {Bruttomesso, R. and Pek, E. and Natasha Sharygina} } @conference { BPST10, title = {The OpenSMT Solver}, booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, volume = {6015}, year = {2010}, pages = {150-153}, publisher = {Springer}, organization = {Springer}, address = {Paphos, Cyprus}, url = {http://dx.doi.org/10.1007/978-3-642-12002-2_12}, author = {Bruttomesso, R. and Pek, E. and Natasha Sharygina and Tsitovich, A.} }