@conference {358,
	title = {Lookahead in Partitioning SMT},
	booktitle = {Formal Methods in Computer-Aided Design - FMCAD 2021},
	year = {2021},
	publisher = {IEEE digital library},
	organization = {IEEE digital library},
	address = {Online Conference},
	abstract = {<p>Lookahead in propositional satisfiability has proven efficient as a heuristic in pre- and in-processing, for partitioning instances for parallel solving, and as the main driver of a standalone solver. While applying similar techniques in satisfiability modulo theories is potentially equally useful, adapting lookahead to learning theory clauses and to estimating search space sizes in the presence of first-order structures is not straightforward. This paper addresses both of these observations. We give a hybrid algorithm that integrates lookahead into the state-based representation of an SMT solver and show that in the vast majority of cases it is possible to compute full lookahead up to depth four on inexpensive theories. We also show the role of first-order structures in SMT search space: while in most of our benchmarks the partitions are easier to solve than the original instance, we identify cases where lookahead results in sequences of increasingly difficult instances for a computationally expensive theory.</p>
},
	author = {Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Natasha Sharygina}
}
@conference {353,
	title = {Lattice-based SMT for program verification},
	booktitle = {International Conference on Formal Methods and Models for System Design, (MEMOCODE)},
	year = {2019},
	publisher = {ACM-IEEE},
	organization = {ACM-IEEE},
	abstract = {<p>We present a lattice-based satisfiability modulo theory for verification of programs with library functions, for which the mathematical libraries supporting these functions contain a high number of equations and inequalities. Common strategies for dealing with library functions include treating them as uninterpreted functions or using the theories under which the functions are fully defined. The full definition could in most cases lead to instances that are too large to solve efficiently. Our lightweight theory uses lattices for efficient representation of library functions by a subset of guarded literals. These lattices are constructed from equations and inequalities of properties of the library functions. These subsets are found during the lattice traversal. We generalise the method to a number of lattices for functions whose values depend on each other in the program, and we describe a simultaneous traversal algorithm of several lattices, so that a combination of guarded literals from all lattices does not lead to contradictory values of their variables. We evaluate our approach on benchmarks taken from the robotics community, and our experimental results demonstrate that we are able to solve a number of instances that were previously unsolvable by existing SMT solvers.</p>
},
	url = {https://dl.acm.org/doi/10.1145/3359986.3361214},
	author = {Karine Even Mendoza and Antti E. J. Hyv{\"a}rinen and Hana Chockler and Natasha Sharygina}
}
@conference {290,
	title = {Lookahead-Based SMT Solving},
	booktitle = {LPAR-22},
	year = {2018},
	month = {November 2018},
	publisher = {EasyChair},
	organization = {EasyChair},
	address = {Awassa, Ethiopia},
	url = {http://www.inf.usi.ch/postdoc/hyvarinen/publications/HyvarinenMSCS_LPAR2018.pdf},
	author = {Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Parvin Sadigova and Hana Chockler and Natasha Sharygina}
}
@conference {279,
	title = {LRA Interpolants from No Man{\textquoteright}s Land},
	booktitle = {Haifa Verification Conference (HVC)},
	year = {2017},
	publisher = {Springer{\textquoteright}s Lecture Notes in Computer Science series (LNCS)},
	organization = {Springer{\textquoteright}s Lecture Notes in Computer Science series (LNCS)},
	author = {Leonardo Alt and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina}
}
