Alloy+HotCore: A fast approximation to unsat core

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...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	D'Ippolito, N., Frias, M.F., Galeotti, J.P., Lanzarotti, E., Mera, S.
Formato:	SER
Materias:	Alloy analyzers Fast approximation Np-completeness SAT-solving Time thresholds Unsatisfiable core Verification problems Abstracting Contour followers Alloys
Acceso en línea:	http://hdl.handle.net/20.500.12110/paper_03029743_v5977LNCS_n_p160_DIppolito
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	todo:paper_03029743_v5977LNCS_n_p160_DIppolito
record_format	dspace
spelling	todo:paper_03029743_v5977LNCS_n_p160_DIppolito2023-10-03T15:19:13Z Alloy+HotCore: A fast approximation to unsat core D'Ippolito, N. Frias, M.F. Galeotti, J.P. Lanzarotti, E. Mera, S. Alloy analyzers Fast approximation Np-completeness SAT-solving Time thresholds Unsatisfiable core Verification problems Abstracting Contour followers Alloys 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. © 2010 Springer. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v5977LNCS_n_p160_DIppolito
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Alloy analyzers Fast approximation Np-completeness SAT-solving Time thresholds Unsatisfiable core Verification problems Abstracting Contour followers Alloys
spellingShingle	Alloy analyzers Fast approximation Np-completeness SAT-solving Time thresholds Unsatisfiable core Verification problems Abstracting Contour followers Alloys D'Ippolito, N. Frias, M.F. Galeotti, J.P. Lanzarotti, E. Mera, S. Alloy+HotCore: A fast approximation to unsat core
topic_facet	Alloy analyzers Fast approximation Np-completeness SAT-solving Time thresholds Unsatisfiable core Verification problems Abstracting Contour followers Alloys
description	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. © 2010 Springer.
format	SER
author	D'Ippolito, N. Frias, M.F. Galeotti, J.P. Lanzarotti, E. Mera, S.
author_facet	D'Ippolito, N. Frias, M.F. Galeotti, J.P. Lanzarotti, E. Mera, S.
author_sort	D'Ippolito, N.
title	Alloy+HotCore: A fast approximation to unsat core
title_short	Alloy+HotCore: A fast approximation to unsat core
title_full	Alloy+HotCore: A fast approximation to unsat core
title_fullStr	Alloy+HotCore: A fast approximation to unsat core
title_full_unstemmed	Alloy+HotCore: A fast approximation to unsat core
title_sort	alloy+hotcore: a fast approximation to unsat core
url	http://hdl.handle.net/20.500.12110/paper_03029743_v5977LNCS_n_p160_DIppolito
work_keys_str_mv	AT dippoliton alloyhotcoreafastapproximationtounsatcore AT friasmf alloyhotcoreafastapproximationtounsatcore AT galeottijp alloyhotcoreafastapproximationtounsatcore AT lanzarottie alloyhotcoreafastapproximationtounsatcore AT meras alloyhotcoreafastapproximationtounsatcore
_version_	1807316689574952960

Alloy+HotCore: A fast approximation to unsat core

Ejemplares similares