{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T11:53:12Z","timestamp":1777636392333,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642405600","type":"print"},{"value":"9783642405617","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40561-7_10","type":"book-chapter","created":{"date-parts":[[2013,9,18]],"date-time":"2013-09-18T13:10:29Z","timestamp":1379509829000},"page":"137-151","source":"Crossref","is-referenced-by-count":2,"title":["Inferring Physical Units in B Models"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Krings","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1007\/11901433_32","volume-title":"Formal Methods and Software Engineering","author":"J.-R. Abrial","year":"2006","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 588\u2013605. Springer, Heidelberg (2006)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-30885-7_13","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"J.-R. Abrial","year":"2012","unstructured":"Abrial, J.-R., Su, W., Zhu, H.: Formalizing hybrid systems with Event-B. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol.\u00a07316, pp. 178\u2013193. Springer, Heidelberg (2012)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Anand, M., Lee, I., Pappas, G., Sokolsky, O.: Unit & dynamic typing in hybrid systems modeling with CHARON. In: Computer Aided Control System Design, pp. 56\u201361. IEEE (2006)","DOI":"10.1109\/CACSD.2006.285444"},{"key":"10_CR6","unstructured":"Back, R.-J., Seceleanu, C.C., Westerholm, J.: Symbolic simulation of hybrid systems. In: Proceedings APSEC 2002, pp. 147\u2013155. IEEE Computer Society (2002)"},{"key":"10_CR7","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. Technical report, Department of Computer Science, University of Iowa (2010), \n                    \n                      http:\/\/www.SMT-LIB.org"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings POPL 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/1039991.1039994","volume":"5","author":"R. Cunis","year":"1992","unstructured":"Cunis, R.: A package for handling units of measure in Lisp. ACM SIGPLAN Lisp Pointers\u00a05, 21\u201325 (1992)","journal-title":"ACM SIGPLAN Lisp Pointers"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Hayes, I.J., Mahony, B.P.: Using units of measurement in formal specifications. Formal Aspects of Computing\u00a07 (1994)","DOI":"10.1007\/BF01211077"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Jiang, L., Su, Z.: Osprey: a practical type system for validating dimensional unit correctness of C programs. In: Proceedings ICSE 2006, pp. 262\u2013271. ACM (2006)","DOI":"10.1145\/1134285.1134323"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-642-17685-2_8","volume-title":"Central European Functional Programming School","author":"A. Kennedy","year":"2010","unstructured":"Kennedy, A.: Types for units-of-measure: Theory and practice. In: Horv\u00e1th, Z., Plasmeijer, R., Zs\u00f3k, V. (eds.) CEFP 2009. LNCS, vol.\u00a06299, pp. 268\u2013305. Springer, Heidelberg (2010)"},{"issue":"3","key":"10_CR13","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1145\/319301.319317","volume":"21","author":"L. Lamport","year":"1999","unstructured":"Lamport, L., Paulson, L.C.: Should your specification language be typed. ACM Trans. Program. Lang. Syst.\u00a021(3), 502\u2013526 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"issue":"2","key":"10_CR15","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M. Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf.\u00a010(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10_CR16","unstructured":"Modelica Association. The Modelica Language Specification version 3.0 (2007)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-642-32759-9_30","volume-title":"FM 2012: Formal Methods","author":"S. Owre","year":"2012","unstructured":"Owre, S., Saha, I., Shankar, N.: Automatic dimensional analysis of cyber-physical systems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol.\u00a07436, pp. 356\u2013371. Springer, Heidelberg (2012)"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer (2010)","DOI":"10.1007\/978-3-642-14509-4"},{"key":"10_CR19","unstructured":"Roy, P., Shankar, N.: SimCheck: An expressive type system for Simulink. In: Proceedings NFM 2010, pp. 149\u2013160. NASA (2010)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Thompson, A., Taylor, B.N.: The International System of Units (SI). Nist Special Publication (2008)","DOI":"10.6028\/NIST.SP.811e2008"},{"key":"10_CR21","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1145\/185009.185036","volume":"29","author":"Z. Umrigar","year":"1994","unstructured":"Umrigar, Z.: Fully static dimensional analysis with C++. ACM SIGPLAN Notices\u00a029, 135\u2013139 (1994)","journal-title":"ACM SIGPLAN Notices"},{"issue":"7","key":"10_CR22","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<605::AID-SPE249>3.0.CO;2-W","volume":"29","author":"A. Delft van","year":"1999","unstructured":"van Delft, A.: A Java extension with support for dimensions. Software: Practice and Experience\u00a029(7), 605\u2013616 (1999)","journal-title":"Software: Practice and Experience"},{"key":"10_CR23","unstructured":"Wand, M., O\u2019Keefe, P.: Automatic dimensional inference. In: Computational Logic: Essays in Honor of Alan Robinson, pp. 479\u2013483 (1991)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40561-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T11:19:26Z","timestamp":1558091966000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40561-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642405600","9783642405617"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40561-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}