{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:03:40Z","timestamp":1725563020399},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642148071"},{"type":"electronic","value":"9783642148088"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14808-8_19","type":"book-chapter","created":{"date-parts":[[2010,8,21]],"date-time":"2010-08-21T05:52:01Z","timestamp":1282369921000},"page":"275-289","source":"Crossref","is-referenced-by-count":2,"title":["Dynamite 2.0: New Features Based on UnSAT-Core Extraction to Improve Verification of Software Requirements"],"prefix":"10.1007","author":[{"given":"Mariano M.","family":"Moscato","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlos G.","family":"L\u00f3pez Pombo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","unstructured":"Arkoudas, K.: Type-\u03c9 DPLs, MIT AI Memo 2001-27 (2001)"},{"key":"19_CR2","volume-title":"Proceedings of RelMiCS 2003","author":"K. Arkoudas","year":"2003","unstructured":"Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M.: Integrating Model Checking and Theorem Proving for Relational Reasoning. In: Proceedings of RelMiCS 2003, Springer, Heidelberg (2003)"},{"key":"19_CR3","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: IJCAR 2010 (to appear, 2010)"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. In: TAP 2009 (2009)","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Dunets, A., Schellhorn, G., Reif, W.: Automated Flaw Detection in Algebraic Specifications. Journal of Automated Reasoning (2010)","DOI":"10.1007\/s10817-010-9166-1"},{"key":"19_CR6","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: MiniSat-p-v1.14. A proof-logging version of MiniSat (September 2006)"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/978-3-540-71209-1_46","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.F. Frias","year":"2007","unstructured":"Frias, M.F., L\u00f3pez Pombo, C.G., Moscato, M.M.: Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 587\u2013601. Springer, Heidelberg (2007)"},{"key":"19_CR8","unstructured":"Hoare, C.A.R., Leavens, G.T., Misra, J., Shankar, N.: The Verified Software Initiative: A Manifesto (2007)"},{"key":"19_CR9","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology\u00a011, 256\u2013290 (2002)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Jackson, D., Schechter, I., Shlyakhter, I.: Alcoa: the Alloy Constraint Analyzer. In: ICSE 2000, pp. 730\u2013733 (2000)","DOI":"10.1145\/337180.337616"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-87603-8_23","volume-title":"Abstract State Machines, B and Z","author":"E. Kang","year":"2008","unstructured":"Kang, E., Jackson, D.: Formal Modeling and Analysis of a Flash Filesystem in Alloy. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol.\u00a05238, pp. 294\u2013308. Springer, Heidelberg (2008)"},{"key":"19_CR12","series-title":"LNAI","first-page":"148","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 148\u2013752. Springer, Heidelberg (1992)"},{"key":"19_CR13","unstructured":"Pudl\u00e1k, P.: Semantic Selection of Premisses for Automated Theorem Proving. In: Proceedings of ESARLT 2007, pp. 27\u201344 (2007)"},{"issue":"1","key":"19_CR14","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s00165-007-0058-z","volume":"20","author":"T. Ramananandro","year":"2008","unstructured":"Ramananandro, T.: Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method. Formal Aspects of Computing\u00a020(1), 21\u201339 (2008)","journal-title":"Formal Aspects of Computing"},{"key":"19_CR15","unstructured":"Sutcliffe, G., Puzis, Y.: SRASS a semantic relevance axiom selection system (2007), \n                    \n                      http:\/\/www.cs.miami.edu\/~tptp\/ATPSystems\/SRASS\/"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-68237-0_23","volume-title":"FM 2008: Formal Methods","author":"E. Torlak","year":"2008","unstructured":"Torlak, E., Chang, F., Jackson, D.: Finding Minimal Unsatisfiable Cores of Declarative Specifications. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 326\u2013341. Springer, Heidelberg (2008)"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A Relational Model Finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"19_CR18","unstructured":"Urban, J.: MaLARea: a Metasystem for Automated Reasoning in Large Theories. In: Proceedings of ESARLT 2007, pp. 45\u201358 (2007)"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Weber, T.: Integrating a SAT Solver with an LCF-style Theorem Prover. In: Proceedings of PDPAR 2005. ENTCS, vol.\u00a0144(2), pp. 67\u201378.","DOI":"10.1016\/j.entcs.2005.12.007"},{"key":"19_CR20","unstructured":"Weber, T.: SAT-based Finite Model Generation for Higher-Order Logic, Ph.D. Thesis, TUM (2008)"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/11813040_23","volume-title":"FM 2006: Formal Methods","author":"P. Zave","year":"2006","unstructured":"Zave, P.: Compositional binding in network domains. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 332\u2013347. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2010"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14808-8_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T17:20:23Z","timestamp":1558286423000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14808-8_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642148071","9783642148088"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14808-8_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}