{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T16:01:33Z","timestamp":1761580893456},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642217678"},{"type":"electronic","value":"9783642217685"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21768-5_12","type":"book-chapter","created":{"date-parts":[[2011,6,27]],"date-time":"2011-06-27T09:18:53Z","timestamp":1309166333000},"page":"152-170","source":"Crossref","is-referenced-by-count":31,"title":["Encoding OCL Data Types for SAT-Based Verification of UML\/OCL Models"],"prefix":"10.1007","author":[{"given":"Mathias","family":"Soeken","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Wille","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","volume-title":"The Unified Modeling Language reference manual","author":"J. Rumbaugh","year":"1999","unstructured":"Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language reference manual. Addison-Wesley Longman, Essex (1999)"},{"issue":"4","key":"12_CR2","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10617-008-9028-9","volume":"12","author":"Y. Vanderperren","year":"2008","unstructured":"Vanderperren, Y., M\u00fcller, W., Dehaene, W.: UML for electronic systems design: a comprehensive overview. Design Automation for Embedded Systems\u00a012(4), 261\u2013292 (2008)","journal-title":"Design Automation for Embedded Systems"},{"key":"12_CR3","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.entcs.2004.09.027","volume":"115","author":"M. Kyas","year":"2005","unstructured":"Kyas, M., Fecher, H., de Boer, F.S., Jacob, J., Hooman, J., van der Zwaag, M., Arons, T., Kugler, H.: Formalizing UML Models and OCL Constraints in PVS. Electronic Notes in Theoretical Computer Science\u00a0115, 39\u201347 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"12_CR4","volume-title":"Verification of Object-Oriented Software: The KeY Approach","author":"B. Beckert","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.: Verification of Object-Oriented Software: The KeY Approach. Springer, Secaucus (2007)"},{"key":"12_CR5","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-02949-3_8","volume-title":"Tests and Proof","author":"M. Gogolla","year":"2009","unstructured":"Gogolla, M., Kuhlmann, M., Hamann, L.: Consistency, Independence and Consequences in UML and OCL Models. In: Tests and Proof, pp. 90\u2013104. Springer, Heidelberg (2009)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: Verification of UML\/OCL Class Diagrams using Constraint Programming. In: IEEE Int. Conf. on Software Testing Verification and Validation Workshop, pp. 73\u201380 (April 2008)","DOI":"10.1109\/ICSTW.2008.54"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-00255-7_4","volume-title":"Integrated Formal Methods","author":"J. Cabot","year":"2009","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: Verifying UML\/OCL Operation Contracts. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol.\u00a05423, pp. 40\u201355. Springer, Heidelberg (2009)"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-540-75209-7_30","volume-title":"Int. Conf. on Model Driven Engineering Languages and Systems","author":"K. Anastasakis","year":"2007","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: A Challenging Model Transformation. In: Int. Conf. on Model Driven Engineering Languages and Systems, pp. 436\u2013450. Springer, Heidelberg (2007)"},{"key":"12_CR9","first-page":"1341","volume-title":"Design, Automation and Test in Europe","author":"M. Soeken","year":"2010","unstructured":"Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML\/OCL models using Boolean satisfiability. In: Design, Automation and Test in Europe, pp. 1341\u20131344. IEEE Computer Society, Los Alamitos (2010)"},{"key":"12_CR10","volume-title":"Design, Automation and Test in Europe","author":"M. Soeken","year":"2011","unstructured":"Soeken, M., Wille, R., Drechsler, R.: Verifying Dynamic Aspects of UML Models. In: Design, Automation and Test in Europe. IEEE Computer Society, Los Alamitos (2011)"},{"key":"12_CR11","volume-title":"The Object Constraint Language: Precise modeling with UML","author":"J. Warmer","year":"1999","unstructured":"Warmer, J., Kleppe, A.: The Object Constraint Language: Precise modeling with UML. Addison-Wesley Longman, Boston (1999)"},{"issue":"3","key":"12_CR12","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1145\/785411.785415","volume":"8","author":"G.A. Constantinides","year":"2003","unstructured":"Constantinides, G.A., Cheung, P.Y.K., Luk, W.: Synthesis of Saturation Arithmetic Architectures. ACM Trans. Design Autom. Electr. Syst.\u00a08(3), 334\u2013354 (2003)","journal-title":"ACM Trans. Design Autom. Electr. Syst."},{"key":"12_CR13","first-page":"151","volume-title":"ACM Symp. on Theory of Computing","author":"S.A. Cook","year":"1971","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: ACM Symp. on Theory of Computing, pp. 151\u2013158. ACM, New York (1971)"},{"key":"12_CR14","first-page":"530","volume-title":"Design Automation Conference","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Design Automation Conference, pp. 530\u2013535. ACM, New York (2001)"},{"key":"12_CR15","first-page":"142","volume-title":"Design, Automation and Test in Europe","author":"E.I. Goldberg","year":"2002","unstructured":"Goldberg, E.I., Novikov, Y.: BerkMin: A Fast and Robust Sat-Solver. In: Design, Automation and Test in Europe, pp. 142\u2013149. IEEE Computer Society, Los Alamitos (2002)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. Theory and Applications of Satisfiability Testing, 502\u2013518 (May 2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"volume-title":"Handbook of Satisfiability","year":"2009","key":"12_CR17","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, February 2009. IOS Press, Amsterdam, NL (February 2009)"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/10720246_8","volume-title":"European Conf. on Planning.","author":"A. Armando","year":"2000","unstructured":"Armando, A., Castellini, C., Giunchiglia, E.: SAT-Based Procedures for Temporal Reasoning. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol.\u00a01809, pp. 97\u2013108. Springer, Heidelberg (2000)"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"12_CR20","first-page":"411","volume-title":"IEEE Symp. on VLSI","author":"R. Wille","year":"2008","unstructured":"Wille, R., Gro\u00dfe, D., Soeken, M., Drechsler, R.: Using Higher Levels of Abstraction for Solving Optimization Problems by Boolean Satisfiability. In: IEEE Symp. on VLSI, pp. 411\u2013416. IEEE Computer Society, Los Alamitos (2008)"},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for Construction and Analysis of Systems","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In: Tools and Algorithms for Construction and Analysis of Systems, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"issue":"7","key":"12_CR22","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1109\/32.538605","volume":"22","author":"D. Jackson","year":"1996","unstructured":"Jackson, D., Damon, C.: Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector. IEEE Trans. on Software Engineering\u00a022(7), 484\u2013495 (1996)","journal-title":"IEEE Trans. on Software Engineering"},{"issue":"1-2","key":"12_CR23","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"J.H. Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real Quantifier Elimination is Doubly Exponential. Journal of Symbolic Computation\u00a05(1-2), 29\u201335 (1988)","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21768-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T07:39:24Z","timestamp":1560325164000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21768-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642217678","9783642217685"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21768-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}