@conference {383,
	title = {CHC Model Validation with Proof Guarantees},
	booktitle = {18th International Conference on integrated Formal Methods (iFM23)},
	year = {2023},
	url = {https://doi.org/10.1007/978-3-031-47705-8_4},
	author = {Rodrigo Otoni and Martin Blicha and Patrick Eugster and Natasha Sharygina}
}
@conference {310,
	title = {A Cooperative Parallelization Approach for Property-Directed k-Induction},
	booktitle = {VMCAI 2020 - 21st International Conference on Verification, Model Checking, and Abstract Interpretation},
	year = {2020},
	address = { New Orleans, USA, 19-25 January 2020},
	doi = {10.1007/978-3-030-39322-9_13},
	author = {Martin Blicha and Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Natasha Sharygina}
}
@conference {293,
	title = {Computing Exact Worst-Case Gas Consumption for Smart Contracts},
	booktitle = {International Symposium on Leveraging Applications of Formal Methods ISoLA 2018: Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice },
	year = {2018},
	publisher = {Springer},
	organization = {Springer},
	address = {Cyprus},
	abstract = {<p>The Ethereum platform is a public, distributed, blockchain-based database that is maintained by independent parties. A user interacts with Ethereum by writing programs and having miners execute them for a fee charged on-the-fly based on the complexity of the execution. The exact fee, measured in gas consumption, in general depends on the unknown Ethereum state, and predicting even its worst case is in principle undecidable. Uncertainty in gas consumption may result in inefficiency, loss of money, and, in extreme cases, in funds being locked for an indeterminate duration. This feasibility study presents two methods for determining the exact worst-case gas consumption of a bounded Ethereum execution using methods influenced by symbolic model checking. We give several concrete cases where gas consumption estimation is needed, and provide two approaches for determining gas consumption, one based on symbolically enumerating execution paths, and the other based on computing paths modularly based on the program structure.</p>
},
	doi = {doi.org/10.1007/978-3-030-03427-6_33},
	url = {https://link.springer.com/chapter/10.1007\%2F978-3-030-03427-6_33},
	author = {Matteo Marescotti and Martin Blicha and Antti E. J. Hyv{\"a}rinen and Sepideh Asadi and Natasha Sharygina}
}
@conference {250,
	title = {Clause Sharing and Partitioning for Cloud-Based SMT Solving},
	booktitle = {ATVA 2016},
	year = {2016},
	url = {http://verify.inf.usi.ch/sites/default/files/ATVA2016.pdf},
	author = {Matteo Marescotti and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina}
}
