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...
Guardado en:
| Publicado: |
2010
|
|---|---|
| Materias: | |
| Acceso en línea: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5977LNCS_n_p160_DIppolito http://hdl.handle.net/20.500.12110/paper_03029743_v5977LNCS_n_p160_DIppolito |
| Aporte de: |
| id |
paper:paper_03029743_v5977LNCS_n_p160_DIppolito |
|---|---|
| record_format |
dspace |
| spelling |
paper:paper_03029743_v5977LNCS_n_p160_DIppolito2023-06-08T15:28:35Z Alloy+HotCore: A fast approximation to unsat core 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. 2010 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5977LNCS_n_p160_DIppolito 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 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. |
| 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 |
| publishDate |
2010 |
| url |
https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5977LNCS_n_p160_DIppolito http://hdl.handle.net/20.500.12110/paper_03029743_v5977LNCS_n_p160_DIppolito |
| _version_ |
1768544272892559360 |