@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}
}
@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 {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.}
}
