Identifying a minimal unsatisfiable core in an Alloy model proved to be a very useful feature in many scenarios. We extend this concept to hot core, an approximation to unsat core that enables the user to obtain valuable feedback when the Alloy’s sat-solving process is abruptly interrupted. We present some use cases that exemplify this new feature and explain the applied heuristics. The NP-completeness nature of the verification problem makes hot core specially appealing, since it is quite frequent for users of the Alloy Analyzer to stop the analysis when some time threshold is exceeded. We provide experimental results showing very promising outcomes supporting our proposal.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{DIppolitoFGLM10,
author = {Nicol{\'{a}}s D'Ippolito and
Marcelo F. Frias and
Juan P. Galeotti and
Esteban Lanzarotti and
Sergio Mera},
editor = {Marc Frappier and
Uwe Gl{\"{a}}sser and
Sarfraz Khurshid and
R{\'{e}}gine Laleau and
Steve Reeves},
title = {Alloy+HotCore: {A} Fast Approximation to Unsat Core},
booktitle = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
{ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5977},
pages = {160--173},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-11811-1\_13},
doi = {10.1007/978-3-642-11811-1\_13},
timestamp = {Mon, 03 Mar 2025 20:58:01 +0100},
biburl = {https://dblp.org/rec/conf/asm/DIppolitoFGLM10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}