@conference {416,
	title = {Parallel SMT Solving via Iterative Tree Partitioning},
	booktitle = {TACAS 2026},
	year = {2026},
	abstract = {We present a novel algorithm for parallel solving of SMT
problems based on a partitioning process that divides the original problem into a tree structure in an iterative way. By enabling node revisiting, the new method addresses the problem of partitioning divergence found in prior approaches that frequently leads to longer runtimes compared to sequential results. The resulting algorithm is highly flexible, offers a combination of partitioning, portfolio solving, and clause sharing, allows the use of various partitioning functions, and scales gracefully with the available resources. We implemented the new approach in the tool SMTS on top of the efficient sequential SMT solver OpenSMT. Our experimental results demonstrate a substantial improvement over OpenSMT in logics QF LRA and QF LIA even when the partitioning approach utilizes just a single solver. Notably, SMTS has consistently dominated several divisions of the annual competition of parallel SMT solvers.},
	author = {Tom{\'a}{\v s} Kol{\'a}rik and Antti E. J. Hyv{\"a}rinen and Seyedmasoud Asadzadeh and Natasha Sharygina}
}
@conference {387,
	title = {Picky CDCL: SMT-solving With Flexible Literal Selection},
	booktitle = {VSTTE},
	year = {2023},
	abstract = {SMT solvers have traditionally been optimized for determining the satisfiability of a query as quickly as possible. However, they are increasingly being used in applications where the time required to determine satisfiability might not be the main concern, such as mining inductive invariants for safety proofs.
This paper studies how lookahead-inspired SMT solving, when made sufficiently efficient and integrated into a conflict-driven, clause learning SMT core, can be a valuable component in a portfolio for proof-based interpolation in model checking.
We implemented the algorithmic idea, called Picky CDCL, in the SMT solver OpenSMT and show its efficiency in the Horn solver Golem using a range of model checking approaches and in SMT proof validation applications.},
	url = {https://link.springer.com/chapter/10.1007/978-3-031-66064-1_1},
	author = {Konstantin I. Britikov and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina}
}
@mastersthesis {332,
	title = {Parallelization and modelling techniques for scalable SMT-based verification},
	volume = {PhD},
	year = {2020},
	month = {01.12.2020},
	school = {USI Lugano},
	abstract = {<p>Software systems are increasingly involved in our daily life tasks, making their failures potentially damaging both in economic and human terms. As a result, proving the correctness of software is widely thought to be one of the most central challenges for computer science. Model checking is an award-winning (Turing award, 2007) technique for formally and automatically verifying systems, often capable to guarantee the correctness of non-trivial and practical programs. However, model checking is undecidable in the general case. Even when properly restricted to the decidable fragment, the algorithms face strong scalability issues preventing them to converge to the solution. The goal of this thesis is to address such scalability issues in two orthogonal ways. First, the design of parallel solving techniques that exploit the massive amount of computational power offered by distributed computing environments. Second, the design of a modelling technique for effective verification of the new emergent technology of smart contracts running on blockchain systems. The parallel solving research efforts consider both bounded and induction-based unbounded model checking, respectively achieved by instantiating multi-agent solving for the T-DPLL and IC3 algorithms. Multi-agent techniques leverage on the diversification and cooperation among sequential solvers executed in parallel. Diversification is achieved with different parallel search heuristics, and cooperation is performed with the exchange of information both during solving time and via upfront agreements. The effectivenesses of various multi-agent settings are empirically evaluated using the purpose-built multi-agent framework SMTS. Verification approaches for emerging technologies tend to either reuse tools for existing languages that often result in inefficient and even unsound models, or to apply generic techniques which typically require human intervention to succeed. This thesis provides a new direct modelling approach using constrained Horn clauses for the emerging technology of smart contracts. Such approach allows automatic solving exploiting the proposed efforts in improving inductive solvers scalability, and guarantees soundness for the safety proofs. Additionally, the smart-contracts-specific task of measuring the amount of computation needed to execute a transaction, i.e. gas consumption, is considered in this thesis proposing an algorithmic solution. The effectiveness of the modelling technique is empirically evaluated over smart contracts deployed in the Ethereum blockchain using an implementation inside the official compiler for the smart contracts language Solidity that relies on the IC3 algorithm.</p>
<p>\&nbsp;</p>
},
	url = {http://verify.inf.usi.ch/sites/default/files/phd_thesis_matteo_marescotti.pdf},
	author = {Matteo Marescotti}
}
@proceedings {240,
	title = {Property Directed Equivalence via Abstract Simulation},
	year = {2016},
	author = {Grigory Fedyukovich and Gurfinkel, A. 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 {222,
	title = {A Proof-Sensitive Approach for Small Propositional Interpolants},
	booktitle = {VSTTE 2015},
	year = {2015},
	url = {http://verify.inf.usi.ch/sites/default/files/main_0.pdf},
	author = {Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina}
}
@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 {180,
	title = {PeRIPLO: A Framework for Producing Efficient Interpolants for SAT-based Software Verification},
	booktitle = {Logic for Programming Artificial Intelligence and Reasoning (LPAR)},
	year = {2013},
	address = {Stellenbosch, South Africa},
	author = {Rollini, S.F. and Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina}
}
@conference {165,
	title = {PINCETTE - Validating Changes and Upgrades in Networked Software},
	booktitle = {17th European Conference on Software Maintenance and Reengineering},
	year = {2013},
	author = {Chockler, H. and Denaro, G. and Ling, M. and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Mariani, L. and Muhammad, A. and Oriol, M. and Rajan, A. and Sery, O. and Natasha Sharygina and Tautschnig, M.}
}
