{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T01:06:28Z","timestamp":1794359188836,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540881933","type":"print"},{"value":"9783540881940","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-88194-0_14","type":"book-chapter","created":{"date-parts":[[2008,10,17]],"date-time":"2008-10-17T10:56:21Z","timestamp":1224240981000},"page":"207-225","source":"Crossref","is-referenced-by-count":1,"title":["Towards Abstraction for DynAlloy Specifications"],"prefix":"10.1007","author":[{"given":"Nazareno M.","family":"Aguirre","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pablo","family":"Ponzio","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Brian J.","family":"Cardiff","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Juan P.","family":"Galeotti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Germ\u00e1n","family":"Regis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b98210","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Das, S., Rajamani, S.: Refining Approximations in Software Predicate Abstraction. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988. Springer, Heidelberg (2004)"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Bjorner, N., Browne, A., Colon, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T.: Verifying Temporal Properties of Reactive Systems: a STeP Tutorial. Formal Methods in System Design\u00a016 (2000)","DOI":"10.1023\/A:1008700623084"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a016(5) (1994)","DOI":"10.1145\/186025.186051"},{"key":"14_CR4","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate Abstraction of ANSI-C Programs using SAT, Technical Report CMU-CS-03-186. Carnegie Mellon University (2003)"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Abstract interpretation. ACM Computing Surveys\u00a028(2) (1996)","DOI":"10.1145\/234528.234740"},{"key":"14_CR6","volume-title":"Proceedings of the IEEE Symposium on Logic in Computer Science LICS 2001","author":"S. Das","year":"2001","unstructured":"Das, S., Dill, D.: Successive Approximation of Abstract Transition Relations. In: Proceedings of the IEEE Symposium on Logic in Computer Science LICS 2001. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X_2","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Das","year":"2002","unstructured":"Das, S., Dill, D.: Counterexample Based Predicate Discovery in Predicate Abstraction. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517. Springer, Heidelberg (2002)"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Dennis, G., Chang, F., Jackson, D.: Modular Verification of Code with SAT. In: Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, pp. 109\u2013120 (2006)","DOI":"10.1145\/1146238.1146251"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Frias, M., L\u00f3pez Pombo, C., Baum, G., Aguirre, N., Maibaum, T.: Reasoning about static and dynamic properties in alloy: A purely relational approach. ACM Transactions on Software Engineering and Methodology (TOSEM)\u00a014(4) (2005)","DOI":"10.1145\/1101815.1101819"},{"key":"14_CR10","volume-title":"Proceedings of the 27th International Conference on Software Engineering ICSE 2005","author":"M. Frias","year":"2005","unstructured":"Frias, M., Galeotti, J.P., L\u00f3pez Pombo, C., Aguirre, N.: DynAlloy: upgrading alloy with actions. In: Proceedings of the 27th International Conference on Software Engineering ICSE 2005. ACM Press, New York (2005)"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Frias, M., Galeotti, J.P., L\u00f3pez Pombo, C., Aguirre, N.: Efficient Analysis of DynAlloy Specifications. In: ACM Transactions on Software Engineering and Methodology (TOSEM). ACM Press, New York","DOI":"10.1145\/1314493.1314497"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, Springer, Heidelberg (1997)"},{"key":"14_CR13","volume-title":"Proceedings of IFIP Working Conference on Software Engineering Techniques (SET 2006)","author":"J.P. Galeotti","year":"2006","unstructured":"Galeotti, J.P., Frias, M.F.: DynAlloy as a Formal Method for the Analysis of Java Programs. In: Proceedings of IFIP Working Conference on Software Engineering Techniques (SET 2006), Warsaw. Springer, Heidelberg (2006)"},{"key":"14_CR14","first-page":"14","volume-title":"Proceedings of the International Symposium on Software Testing and Analysis (ISSTA)","author":"D. Jackson","year":"2000","unstructured":"Jackson, D., Vaziri, M.: Finding Bugs with a Constraint Solver. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), Portland, OR, USA, August 21-24, pp. 14\u201325. ACM Press, New York (2000)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology (ACM TOSEM)\u00a011(2) (2002)","DOI":"10.1145\/505145.505149"},{"key":"14_CR16","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"\u00abUML\u00bb \u201999 - The Unified Modeling Language. Beyond the Standard","author":"S.-K. Kim","year":"1999","unstructured":"Kim, S.-K., Carrington, D.: Formalizing the UML Class Diagram Using Object-Z. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol.\u00a01723. Springer, Heidelberg (1999)"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Snook, C., Butler, M.: UML-B: Formal modeling and design aided by UML. ACM Transactions on Software Engineering and Methodology (TOSEM)\u00a015(1) (2006)","DOI":"10.1145\/1125808.1125811"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Taghdiri, M.: Inferring Specifications to Detect Errors in Code. In: Proceedings of the 19th International Conference on Automated Software Engineering ASE 2004, Austria (September 2004)","DOI":"10.1109\/ASE.2004.1342732"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_44","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Uchitel","year":"2003","unstructured":"Uchitel, S., Chatley, R., Kramer, J., Magee, J.: LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619. Springer, Heidelberg (2003)"},{"key":"14_CR21","volume-title":"Using Z: Specification, Refinement and Proof","author":"J. Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice-Hall, Englewood Cliffs (1996)"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Saturn: A Scalable Framework for Error Detection Using Boolean Satisfiability. ACM-Transactions on Programming Languages and Systems (TOPLAS) (to appear)","DOI":"10.1145\/1232420.1232423"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88194-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T15:08:04Z","timestamp":1557846484000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88194-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540881933","9783540881940"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88194-0_14","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-540-88194-0","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}