Navegar

Colección

Datos Estadísticas

Artículo

D'Ippolito, N.; Frias, M.F.; Galeotti, J.P.; Lanzarotti, E.; Mera, S. "Alloy+HotCore: A fast approximation to unsat core" (2010) 2nd International Conference on Abstract State Machines, Alloy, B and Z, ABZ 2010. 5977 LNCS:160-173
El editor solo permite decargar el artículo en su versión post-print desde el repositorio. Por favor, si usted posee dicha versión, enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

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.

Registro:

Documento: Artículo
Título:Alloy+HotCore: A fast approximation to unsat core
Autor:D'Ippolito, N.; Frias, M.F.; Galeotti, J.P.; Lanzarotti, E.; Mera, S.
Ciudad:Orford, QC
Filiación:Departamento de Computación, UBA, Argentina
Palabras clave:Alloy analyzers; Fast approximation; Np-completeness; SAT-solving; Time thresholds; Unsatisfiable core; Verification problems; Abstracting; Contour followers; Alloys
Año:2010
Volumen:5977 LNCS
Página de inicio:160
Página de fin:173
DOI: http://dx.doi.org/10.1007/978-3-642-11811-1_13
Título revista:2nd International Conference on Abstract State Machines, Alloy, B and Z, ABZ 2010
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5977LNCS_n_p160_DIppolito

Referencias:

  • Jackson, D., (2006) Software Abstractions: Logic, Language, and Analysis, , MIT Press, Cambridge
  • Een, N., Sorensson, N., An extensible SAT-solver (2004) LNCS, 2919, pp. 502-518. , Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. Springer, Heidelberg
  • Torlak, E., Chang, F., Jackson, D., Finding minimal unsatisfiable cores of declarative specifications (2008) LNCS, 5014, pp. 326-341. , Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. Springer, Heidelberg
  • Cook, S.A., The complexity of theorem-proving procedures STOC 1971, 1971, pp. 151-158. , ACM, New York
  • Sinz, C., Visualizing sat instances and runs of the dpll algorithm (2007) Journal of Automated Reasoning, 39 (2), pp. 219-243
  • Selman, B., Levesque, H., Mitchell, D., A new method for solving hard satisfiability problems (1992) Procs. of the 10th Conf. on Artificial Intelligence, pp. 440-446
  • Selman, B., Kautz, H., Cohen, B., Local search strategies for satisfiability testing (1993) DIMACS Series in Discrete Mathematics and Theoretical Computer Science
  • Mazure, B., Saïs, L., Grégoire, É., A powerful heuristic to locate inconsistent kernels in knowledge-based systems (1996) IPMU 1996, pp. 1265-1269
  • Grégoire, E., Mazure, B., Piette, C., Boosting a complete technique to find mss and mus thanks to a local search oracle (2007) Proceedings of IJCAI, pp. 2300-2305
  • Leino, K.R.M., Müller, P., Object invariants in dynamic contexts (2004) LNCS, 3086, pp. 491-515. , Odersky, M. (ed.) ECOOP 2004. Springer, Heidelberg
  • Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D., (2002) Evaluating the Small Scope Hypothesis, , http://sdg.csail.mit.edu/pubs/2002/SSH.pdf
  • Davis, M., Logemann, G., Loveland, D., A machine program for theorem-proving (1962) Commun. ACM, 5 (7), pp. 394-397
  • Silva, J.P.M., Sakallah, K.A., GRASP - A new search algorithm for satisfiability (1997) 1996 IEEE/ACM International Conference on Computer-aided Design, pp. 220-227. , IEEE Computer Society, Washington
  • Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S., Chaff: Engineering an efficient SAT solver (2001) Design Automation Conference, pp. 530-535
  • Marques-Silva, J., The impact of branching heuristics in propositional satisfiability algorithms (1999) LNCS (LNAI), 1695, pp. 62-74. , Barahona, P., Alferes, J.J. (eds.) EPIA 1999. Springer, Heidelberg
  • Goldberg, E., Novikov, Y., BerkMin: A fast and robust SAT-solver (2007) Discrete Applied Mathematics, 155 (12), pp. 1549-1561
  • Zhang, L., Malik, S., Extracting small unsatisfiable cores from unsatisfiable boolean formulas (2003) Proceedings of SAT, 3
  • Bruni, R., Sassano, A., Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae (2001) ENDM, 9, pp. 162-173
  • Torlak, E., Jackson, D., Kodkod: A relational model finder (2007) LNCS, 4424, pp. 632-647. , Grumberg, O., Huth, M. (eds.) TACAS 2007. Springer, Heidelberg
  • Galeotti, J., Distributed sat-based analysis of object oriented code Proceedings of Symposium on Automatic Program Verification (APV 2009), Rio Cuarto, Argentina, ETH Zurich (February 2009)

Citas:

---------- APA ----------
D'Ippolito, N., Frias, M.F., Galeotti, J.P., Lanzarotti, E. & Mera, S. (2010) . Alloy+HotCore: A fast approximation to unsat core. 2nd International Conference on Abstract State Machines, Alloy, B and Z, ABZ 2010, 5977 LNCS, 160-173.
http://dx.doi.org/10.1007/978-3-642-11811-1_13
---------- CHICAGO ----------
D'Ippolito, N., Frias, M.F., Galeotti, J.P., Lanzarotti, E., Mera, S. "Alloy+HotCore: A fast approximation to unsat core" . 2nd International Conference on Abstract State Machines, Alloy, B and Z, ABZ 2010 5977 LNCS (2010) : 160-173.
http://dx.doi.org/10.1007/978-3-642-11811-1_13
---------- MLA ----------
D'Ippolito, N., Frias, M.F., Galeotti, J.P., Lanzarotti, E., Mera, S. "Alloy+HotCore: A fast approximation to unsat core" . 2nd International Conference on Abstract State Machines, Alloy, B and Z, ABZ 2010, vol. 5977 LNCS, 2010, pp. 160-173.
http://dx.doi.org/10.1007/978-3-642-11811-1_13
---------- VANCOUVER ----------
D'Ippolito, N., Frias, M.F., Galeotti, J.P., Lanzarotti, E., Mera, S. Alloy+HotCore: A fast approximation to unsat core. Lect. Notes Comput. Sci. 2010;5977 LNCS:160-173.
http://dx.doi.org/10.1007/978-3-642-11811-1_13