{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,26]],"date-time":"2026-10-26T17:50:44Z","timestamp":1793037044861,"version":"4.5.0"},"publisher-location":"New York, NY, USA","reference-count":140,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2006,10,22]]},"DOI":"10.1145\/1173706.1173740","type":"proceedings-article","created":{"date-parts":[[2007,1,17]],"date-time":"2007-01-17T01:15:56Z","timestamp":1168996556000},"page":"221-236","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":42,"title":["Roadmap for enhanced languages and methods to aid verification"],"prefix":"10.1145","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[{"name":"Iowa State University, Ames, IA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Raymond","family":"Abrial","sequence":"additional","affiliation":[{"name":"ETH Z\u00fcrich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Don","family":"Batory","sequence":"additional","affiliation":[{"name":"University of Texas, Austin, TX"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Butler","sequence":"additional","affiliation":[{"name":"University of Southampton, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Coglio","sequence":"additional","affiliation":[{"name":"Kestrel Institute, CA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kathi","family":"Fisler","sequence":"additional","affiliation":[{"name":"Worcester Polytechnic Institute, MA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eric","family":"Hehner","sequence":"additional","affiliation":[{"name":"University of Toronto, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cliff","family":"Jones","sequence":"additional","affiliation":[{"name":"Newcastle, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dale","family":"Miller","sequence":"additional","affiliation":[{"name":"INRIA-Futurs, Polytechnique, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Simon","family":"Peyton-Jones","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Murali","family":"Sitaraman","sequence":"additional","affiliation":[{"name":"Clemson University, SC"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Douglas R.","family":"Smith","sequence":"additional","affiliation":[{"name":"Kestrel Institute, CA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[{"name":"Washington University of St. Louis, MO"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2006,10,22]]},"reference":[{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/236705"},{"key":"e_1_3_2_1_4_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027227","volume-title":"Formal Methods for Industrial Applications, Specifying and Programming the Steam Boiler Control","author":"Abrial J.-R.","year":"1996","unstructured":"J.-R. Abrial , E. B\u00f6rger , and H. Langmaack , editors . Formal Methods for Industrial Applications, Specifying and Programming the Steam Boiler Control , volume 1165 of Lecture Notes in Computer Science . Springer-Verlag , 1996 .]] J.-R. Abrial, E. B\u00f6rger, and H. Langmaack, editors. Formal Methods for Industrial Applications, Specifying and Programming the Steam Boiler Control, volume 1165 of Lecture Notes in Computer Science. Springer-Verlag, 1996.]]"},{"key":"e_1_3_2_1_5_1","volume-title":"XXI","author":"Abrial J.-R.","year":"2006","unstructured":"J.-R. Abrial and S. Hallerstede . Refinement, decomposition, and instantiation of discrete models: Application to Event-B. Fundamenta Informaticae , XXI , 2006 .]] J.-R. Abrial and S. Hallerstede. Refinement, decomposition, and instantiation of discrete models: Application to Event-B. Fundamenta Informaticae, XXI, 2006.]]"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2006.5.5.a3"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/390017.808306"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/b13229"},{"key":"e_1_3_2_1_9_1","volume-title":"Oct.","author":"Team J","year":"2004","unstructured":"Aspect J Team . The AspectJ programming guide. Available from http:\/\/eclipse.org\/aspectj , Oct. 2004 .]] AspectJ Team. The AspectJ programming guide. Available from http:\/\/eclipse.org\/aspectj, Oct. 2004.]]"},{"key":"e_1_3_2_1_10_1","first-page":"51","volume-title":"Formal Description of Programming Concepts, IFIP State-of-the-Art Reports","author":"Astesiano E.","year":"1991","unstructured":"E. Astesiano . Inductive and operational semantics . In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts, IFIP State-of-the-Art Reports , pages 51 -- 136 . Springer-Verlag , New York, NY , 1991 .]] E. Astesiano. Inductive and operational semantics. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts, IFIP State-of-the-Art Reports, pages 51--136. Springer-Verlag, New York, NY, 1991.]]"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_2_1_13_1","unstructured":"B-Core (UK) Limited. B-toolkit manuals. http:\/\/www.b-core.com 1999.]]  B-Core (UK) Limited. B-toolkit manuals. http:\/\/www.b-core.com 1999.]]"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science","author":"Back R.-J.","year":"1998","unstructured":"R.-J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science . Springer-Verlag , 1998 .]] R.-J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer-Verlag, 1998.]]"},{"key":"e_1_3_2_1_15_1","volume-title":"J. W. de Bakker, W.-P","author":"Back R. J. R.","year":"1990","unstructured":"R. J. R. Back . Refinement calculus , part II: Parallel and reactive programs . In J. W. de Bakker, W.-P . de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, LNCS 430. Springer-Verlag , 1990 .]] R. J. R. Back. Refinement calculus, part II: Parallel and reactive programs. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, LNCS 430. Springer-Verlag, 1990.]]"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90069-P"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90069-P"},{"key":"e_1_3_2_1_18_1","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"Barnes J.","year":"2003","unstructured":"J. Barnes . High Integrity Software: The SPARK Approach to Safety and Security . Addison Wesley , New York, NY , 2003 .]] J. Barnes. High Integrity Software: The SPARK Approach to Safety and Security. Addison Wesley, New York, NY, 2003.]]"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.453.0527"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.23"},{"key":"e_1_3_2_1_23_1","volume-title":"Kestrel Technology","author":"Becker M.","year":"2003","unstructured":"M. Becker , L. Gilham , and D. R. Smith . Planware II: Synthesis of schedulers for complex resource systems. Technical report , Kestrel Technology , 2003 .]] M. Becker, L. Gilham, and D. R. Smith. Planware II: Synthesis of schedulers for complex resource systems. Technical report, Kestrel Technology, 2003.]]"},{"key":"e_1_3_2_1_24_1","volume-title":"Casl User Manual. LNCS 2900 (IFIP Series)","author":"Bidoit M.","year":"2004","unstructured":"M. Bidoit and P. D. Mosses . Casl User Manual. LNCS 2900 (IFIP Series) . Springer-Verlag , 2004 .]] M. Bidoit and P. D. Mosses. Casl User Manual. LNCS 2900 (IFIP Series). Springer-Verlag, 2004.]]"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/4472.4474"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-002-0013-7"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2932433.2932497"},{"key":"e_1_3_2_1_28_1","first-page":"1045","volume-title":"Fifth International Joint Conference on Artifical Intelligence, MIT","volume":"2","author":"Burstall R. M.","unstructured":"R. M. Burstall and J. A. Goguen . Putting theories together to make specifications . In Fifth International Joint Conference on Artifical Intelligence, MIT , Cambridge, Mass. , volume 2 , pages 1045 -- 1058 . IJCAI-77, Department of Computer Science, Carnegie Mellon, Pittsburgh, Aug. 1977.]] R. M. Burstall and J. A. Goguen. Putting theories together to make specifications. In Fifth International Joint Conference on Artifical Intelligence, MIT, Cambridge, Mass., volume 2, pages 1045--1058. IJCAI-77, Department of Computer Science, Carnegie Mellon, Pittsburgh, Aug. 1977.]]"},{"key":"e_1_3_2_1_29_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/3-540-10007-5_41","volume-title":"Abstract Software Specification","author":"Burstall R. M.","year":"1980","unstructured":"R. M. Burstall and J. A. Goguen . The semantics of CLEAR, a specification language . In Abstract Software Specification , Copenhagen Winter School, volume 86 of Lecture Notes in Computer Science , pages 292 -- 332 . Springer-Verlag , New York, NY, 1980 . Also University of Edinburgh, Department of Computer Science, Internal Report, CSR-65-80, Feb, 1980.]] R. M. Burstall and J. A. Goguen. The semantics of CLEAR, a specification language. In Abstract Software Specification, Copenhagen Winter School, volume 86 of Lecture Notes in Computer Science, pages 292--332. Springer-Verlag, New York, NY, 1980. Also University of Edinburgh, Department of Computer Science, Internal Report, CSR-65-80, Feb, 1980.]]"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(96)81173-7"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200025"},{"key":"e_1_3_2_1_32_1","first-page":"129","volume-title":"Abrial et al. {4} FMIA95","author":"Butler M. J.","unstructured":"M. J. Butler , E. Sekerinski , and K. Sere . An action system approach to the steam boiler problem . In Abrial et al. {4} FMIA95 , pages 129 -- 148 .]] M. J. Butler, E. Sekerinski, and K. Sere. An action system approach to the steam boiler problem. In Abrial et al. {4} FMIA95, pages 129--148.]]"},{"key":"e_1_3_2_1_33_1","volume-title":"Workshop on Formal Techniques for Java-like Programs (FTfJP)","author":"Charles J.","year":"2006","unstructured":"J. Charles . Adding native specifications to JML . In Workshop on Formal Techniques for Java-like Programs (FTfJP) , July 2006 .]] J. Charles. Adding native specifications to JML. In Workshop on Formal Techniques for Java-like Programs (FTfJP), July 2006.]]"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086375"},{"key":"e_1_3_2_1_35_1","unstructured":"ClearSy. Atelier B user and reference manuals. http:\/\/tinyurl.com\/lkj72 1996.]]  ClearSy. Atelier B user and reference manuals. http:\/\/tinyurl.com\/lkj72 1996.]]"},{"key":"e_1_3_2_1_36_1","volume-title":"Proc. IFIP Working Conference on Verified Software: Tools, Techniques, and Experiments","author":"Coglio A.","year":"2005","unstructured":"A. Coglio and C. Green . A constructive approach to correctness, exemplified by a generator for certified Java Card appplets . In Proc. IFIP Working Conference on Verified Software: Tools, Techniques, and Experiments , Oct. 2005 .]] A. Coglio and C. Green. A constructive approach to correctness, exemplified by a generator for certified Java Card appplets. In Proc. IFIP Working Conference on Verified Software: Tools, Techniques, and Experiments, Oct. 2005.]]"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349315"},{"key":"e_1_3_2_1_38_1","series-title":"NATO ASI Series","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/978-3-642-74884-4_3","volume-title":"Constructive Methods in Computing Science","author":"Constable R. L.","year":"1989","unstructured":"R. L. Constable . Assigning meaning to proofs: a semantic basis for problem solving environments . In M. Broy, editor, Constructive Methods in Computing Science , volume F 55 of NATO ASI Series , pages 63 -- 91 . Springer-Verlag , New York, NY , 1989 .]] R. L. Constable. Assigning meaning to proofs: a semantic basis for problem solving environments. In M. Broy, editor, Constructive Methods in Computing Science, volume F55 of NATO ASI Series, pages 63--91. Springer-Verlag, New York, NY, 1989.]]"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_3_2_1_40_1","volume-title":"Generative Programming: Methods, Tools, and Applications","author":"Czarnecki K.","year":"2000","unstructured":"K. Czarnecki and U. W. Eisenecker . Generative Programming: Methods, Tools, and Applications . Addison-Wesley , 2000 .]] K. Czarnecki and U. W. Eisenecker. Generative Programming: Methods, Tools, and Applications. Addison-Wesley, 2000.]]"},{"key":"e_1_3_2_1_41_1","unstructured":"CZT Partners. Community Z tools. http:\/\/czt.sourceforge.net\/ 2006.]]  CZT Partners. Community Z tools. http:\/\/czt.sourceforge.net\/ 2006.]]"},{"key":"e_1_3_2_1_42_1","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511663079","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"de Roever W.-P.","year":"1998","unstructured":"W.-P. de Roever and K. Engelhardt . Data Refinement: Model-Oriented Proof Methods and their Comparison , volume 47 of Cambridge Tracts in Theoretical Computer Science . Cambridge University Press , New York, NY , 1998 .]] W.-P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison, volume 47 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, New York, NY, 1998.]]"},{"key":"e_1_3_2_1_43_1","series-title":"Lecture Notes in Computer Science","volume-title":"Compositionality: The Significant Difference","author":"de Roever W. P.","year":"1997","unstructured":"W. P. de Roever , H. Langmaack , and A. Pnueli , editors . Compositionality: The Significant Difference , International Symposium , COMPOS'97, Bad Malente, Germany, September 8-12, 1997 . Revised Lectures, volume 1536 of Lecture Notes in Computer Science . Springer-Verlag , 1998.]] W. P. de Roever, H. Langmaack, and A. Pnueli, editors. Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures, volume 1536 of Lecture Notes in Computer Science. Springer-Verlag, 1998.]]"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/190679.190682"},{"key":"e_1_3_2_1_46_1","series-title":"EATCS Monographs on Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69962-7","volume-title":"Fundamentals of Algebraic Specification 1: Equations and Initial Semantics","author":"Ehrig H.","year":"1985","unstructured":"H. Ehrig and B. Mahr . Fundamentals of Algebraic Specification 1: Equations and Initial Semantics , volume 6 of EATCS Monographs on Theoretical Computer Science . Springer-Verlag , New York, NY , 1985 .]] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, New York, NY, 1985.]]"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/1251229.1251230"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/249069.231389"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/949305.949332"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.485225"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004562"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"crossref","unstructured":"C.\n      Flanagan\n     and \n      K. R. M.\n      Leino\n    . Houdini an annotation assistant for ESC\/Java\n  . In J. N. Oliveira and P. Zave editors FME \n  2001\n  : Formal Methods for Increasing Software Productivity volume \n  2021\n   of \n  Lecture Notes in Computer Science pages \n  500\n  --\n  517\n  . \n  Springer Mar. 2001.]]   C. Flanagan and K. R. M. Leino. Houdini an annotation assistant for ESC\/Java. In J. N. Oliveira and P. Zave editors FME 2001: Formal Methods for Increasing Software Productivity volume 2021 of Lecture Notes in Computer Science pages 500--517. Springer Mar. 2001.]]","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318610"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/547173"},{"key":"e_1_3_2_1_56_1","first-page":"80","volume-title":"Current Trends in Programming Methodology","author":"Goguen J. A.","year":"1978","unstructured":"J. A. Goguen , J. W. Thatcher , and E. G. Wagner . An initial algebra approach to the specification, correctness and implementation of abstract data types . In R. T. Yeh, editor, Current Trends in Programming Methodology , volume 4 , pages 80 -- 149 . Prentice-Hall, Inc. , Englewood Cliffs, N.J. , 1978 .]] J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. In R. T. Yeh, editor, Current Trends in Programming Methodology, volume 4, pages 80--149. Prentice-Hall, Inc., Englewood Cliffs, N.J., 1978.]]"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00260922"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/151155"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_3_2_1_60_1","first-page":"154","volume-title":"Araki et al. \\citeFME03","author":"Hayes I. J.","unstructured":"I. J. Hayes , M. Jackson , and C. B. Jones . Determining the specification of a control system from that of its environment . In Araki et al. \\citeFME03 , pages 154 -- 169 .]] I. J. Hayes, M. Jackson, and C. B. Jones. Determining the specification of a control system from that of its environment. In Araki et al. \\citeFME03, pages 154--169.]]"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/154690"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050017"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.006"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/27651.27653"},{"key":"e_1_3_2_1_68_1","volume-title":"Proc. IFIP Working Conference on Verified Software: Tools, Techniques, and Experiments","author":"Hoare C. A. R.","year":"2005","unstructured":"C. A. R. Hoare , N. Shankar , and J. Misra , editors . Proc. IFIP Working Conference on Verified Software: Tools, Techniques, and Experiments , Z\u00fcrich, Switzerland , Oct. 2005 .]] C. A. R. Hoare, N. Shankar, and J. Misra, editors. Proc. IFIP Working Conference on Verified Software: Tools, Techniques, and Experiments, Z\u00fcrich, Switzerland, Oct. 2005.]]"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/602382.602403"},{"key":"e_1_3_2_1_70_1","unstructured":"T. Hoare J. Misra and N. Shankar. The IFIP working conference on verified software: Theories tools experiments. http:\/\/tinyurl.com\/nrhdl Oct. 2005.]]  T. Hoare J. Misra and N. Shankar. The IFIP working conference on verified software: Theories tools experiments. http:\/\/tinyurl.com\/nrhdl Oct. 2005.]]"},{"key":"e_1_3_2_1_72_1","first-page":"479","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Howard W. A.","year":"1980","unstructured":"W. A. Howard . The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism , pages 479 -- 490 . Academic Press, Inc. , New York, NY , 1980 .]] W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479--490. Academic Press, Inc., New York, NY, 1980.]]"},{"key":"e_1_3_2_1_73_1","unstructured":"R. Inc. Software Refinery Mar. 2006. http:\/\/www.reasoning.com\/.]]  R. Inc. Software Refinery Mar. 2006. http:\/\/www.reasoning.com\/.]]"},{"key":"e_1_3_2_1_74_1","volume-title":"The Language. The Standard Libraries","author":"International Organization for Standardization.","year":"1995","unstructured":"International Organization for Standardization. Ada 95 Reference Manual . The Language. The Standard Libraries , Jan. 1995 . ANSI\/ISO\/IEC-8652:1995.]] International Organization for Standardization. Ada 95 Reference Manual. The Language. The Standard Libraries, Jan. 1995. ANSI\/ISO\/IEC-8652:1995.]]"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/286942.286973"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0261-2","volume-title":"PASCAL User Manual and Report","author":"Jensen K.","year":"1985","unstructured":"K. Jensen and N. Wirth . PASCAL User Manual and Report ( third edition). Springer-Verlag , New York, NY , 1985 . Revised to the ISO Standard by Andrew B. Mickel and James F. Miner.]] K. Jensen and N. Wirth. PASCAL User Manual and Report (third edition). Springer-Verlag, New York, NY, 1985. Revised to the ISO Standard by Andrew B. Mickel and James F. Miner.]]"},{"key":"e_1_3_2_1_77_1","volume-title":"International Series in Computer Science","author":"Jones C. B.","year":"1990","unstructured":"C. B. Jones . Systematic Software Development Using VDM. International Series in Computer Science . Prentice Hall, Englewood Cliffs , N.J. , second edition, 1990 .]] C. B. Jones. Systematic Software Development Using VDM. International Series in Computer Science. Prentice Hall, Englewood Cliffs, N.J., second edition, 1990.]]"},{"key":"e_1_3_2_1_79_1","volume-title":"Specware System and documentation","author":"Kestrel Development Corporation","year":"2004","unstructured":"Kestrel Development Corporation . Specware System and documentation , 2004 . http:\/\/www.specware.org\/.]] Kestrel Development Corporation. Specware System and documentation, 2004. http:\/\/www.specware.org\/.]]"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"crossref","unstructured":"G.\n      Kiczales E.\n      Hilsdale J.\n      Hugunin M.\n      Kersten J.\n      Palm and \n      W. G.\n      Griswold\n  . \n  An overview of AspectJ\n  . In J. L. Knudsen editor ECOOP \n  2001\n   --- Object-Oriented Programming 15th European Conference Budapest Hungary volume \n  2072\n   of \n  Lecture Notes in Computer Science pages \n  327\n  --\n  353\n  . \n  Springer-Verlag Berlin June 2001.]]   G. Kiczales E. Hilsdale J. Hugunin M. Kersten J. Palm and W. G. Griswold. An overview of AspectJ. In J. L. Knudsen editor ECOOP 2001 --- Object-Oriented Programming 15th European Conference Budapest Hungary volume 2072 of Lecture Notes in Computer Science pages 327--353. Springer-Verlag Berlin June 2001.]]","DOI":"10.1007\/3-540-45337-7_18"},{"key":"e_1_3_2_1_81_1","first-page":"60","volume-title":"ACM OOPSLA Workshop on Specification and Verification of Component-Based Systems (SAVCBS)","author":"Krone J.","year":"2001","unstructured":"J. Krone , W. F. Ogden , and M. Sitaraman . Modular verification of performance constraints . In ACM OOPSLA Workshop on Specification and Verification of Component-Based Systems (SAVCBS) , pages 60 -- 67 , 2001 .]] J. Krone, W. F. Ogden, and M. Sitaraman. Modular verification of performance constraints. In ACM OOPSLA Workshop on Specification and Verification of Component-Based Systems (SAVCBS), pages 60--67, 2001.]]"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/63238.63240"},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2004.1293079"},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.05.015"},{"key":"e_1_3_2_1_87_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/978-3-540-24851-4_22","volume-title":"European Conference on Object-Oriented Programming (ECOOP)","author":"Leino K. R. M.","year":"2004","unstructured":"K. R. M. Leino and P. M\u00fcller . Object invariants in dynamic contexts . In M. Odersky, editor, European Conference on Object-Oriented Programming (ECOOP) , volume 3086 of Lecture Notes in Computer Science , pages 491 -- 516 . Springer-Verlag , June 2004 .]] K. R. M. Leino and P. M\u00fcller. Object invariants in dynamic contexts. In M. Odersky, editor, European Conference on Object-Oriented Programming (ECOOP), volume 3086 of Lecture Notes in Computer Science, pages 491--516. Springer-Verlag, June 2004.]]"},{"key":"e_1_3_2_1_88_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis, 7th International Symposium, SAS","author":"Lev-Ami T.","year":"2000","unstructured":"T. Lev-Ami and S. Sagiv . TVLA: A system for implementing static analyses . In J. Palsberg, editor, Static Analysis, 7th International Symposium, SAS 2000 , Proceedings, volume 1824 of Lecture Notes in Computer Science , pages 280 -- 301 . Springer , 2000.]] T. Lev-Ami and S. Sagiv. TVLA: A system for implementing static analyses. In J. Palsberg, editor, Static Analysis, 7th International Symposium, SAS 2000, Proceedings, volume 1824 of Lecture Notes in Computer Science, pages 280--301. Springer, 2000.]]"},{"key":"e_1_3_2_1_89_1","volume-title":"Abstraction and Specification in Program Development","author":"Liskov B.","year":"1986","unstructured":"B. Liskov and J. Guttag . Abstraction and Specification in Program Development . The MIT Press, Cambridge , Mass ., 1986 .]] B. Liskov and J. Guttag. Abstraction and Specification in Program Development. The MIT Press, Cambridge, Mass., 1986.]]"},{"key":"e_1_3_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/359763.359789"},{"key":"e_1_3_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01786229"},{"key":"e_1_3_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.5555\/647639.733229"},{"key":"e_1_3_2_1_93_1","volume-title":"Abstraction and verification in Alphard: a symbol table example. Technical report","author":"London R. L.","year":"1976","unstructured":"R. L. London , M. Shaw , and W. A. Wulf . Abstraction and verification in Alphard: a symbol table example. Technical report , Information Sciences Institute , USC , Dec. 1976 .]] R. L. London, M. Shaw, and W. A. Wulf. Abstraction and verification in Alphard: a symbol table example. Technical report, Information Sciences Institute, USC, Dec. 1976.]]"},{"key":"e_1_3_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_3_2_1_95_1","unstructured":"Matisse Partners. Matisse: Methodologies and technologies for industrial strength systems engineering. http:\/\/www.matisse.qinetiq.com\/ 2003.]]  Matisse Partners. Matisse: Methodologies and technologies for industrial strength systems engineering. http:\/\/www.matisse.qinetiq.com\/ 2003.]]"},{"key":"e_1_3_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111068"},{"key":"e_1_3_2_1_98_1","series-title":"Object-Oriented Series","volume-title":"The Language","author":"Meyer B.","year":"1992","unstructured":"B. Meyer . Eiffel : The Language . Object-Oriented Series . Prentice Hall , New York, NY , 1992 .]] B. Meyer. Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York, NY, 1992.]]"},{"key":"e_1_3_2_1_99_1","volume-title":"NY","author":"Meyer B.","year":"1997","unstructured":"B. Meyer . Object-oriented Software Construction . Prentice Hall , New York , NY , second edition, 1997 .]] B. Meyer. Object-oriented Software Construction. Prentice Hall, New York, NY, second edition, 1997.]]"},{"key":"e_1_3_2_1_100_1","volume-title":"Prentice Hall International","author":"Morgan C.","year":"1994","unstructured":"C. Morgan . Programming from Specifications: Second Edition . Prentice Hall International , Hempstead, UK , 1994 .]] C. Morgan. Programming from Specifications: Second Edition. Prentice Hall International, Hempstead, UK, 1994.]]"},{"key":"e_1_3_2_1_101_1","series-title":"Formal approaches of computing and information technology series","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-3273-8","volume-title":"On the refinement calculus","author":"Morgan C.","year":"1994","unstructured":"C. Morgan and T. Vickers , editors . On the refinement calculus . Formal approaches of computing and information technology series . Springer-Verlag , New York, NY , 1994 .]] C. Morgan and T. Vickers, editors. On the refinement calculus. Formal approaches of computing and information technology series. Springer-Verlag, New York, NY, 1994.]]"},{"key":"e_1_3_2_1_102_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380100402"},{"key":"e_1_3_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_3_2_1_104_1","doi-asserted-by":"crossref","unstructured":"P.\n      M\u00fcller\n      . \n      Modular\n      Specification\n     and \n      Verification\n       of \n      Object-Oriented Programs volume \n  2262\n   of \n  Lecture Notes in Computer Science\n  . \n  Springer-Verlag 2002\n  .]]  P. M\u00fcller. Modular Specification and Verification of Object-Oriented Programs volume 2262 of Lecture Notes in Computer Science. Springer-Verlag 2002.]]","DOI":"10.1007\/3-540-45651-1"},{"key":"e_1_3_2_1_105_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.713"},{"key":"e_1_3_2_1_107_1","volume-title":"5th International Workshop on Graph Transformation and Visual Modeling Techniques","author":"Narayanan A.","year":"2006","unstructured":"A. Narayanan and G. Karsai . Towards verifying model transformations. In R. Bruni and D. Varr\u00f3, editors , 5th International Workshop on Graph Transformation and Visual Modeling Techniques , Vienna, pages 185- -194, Apr 2006 .]] A. Narayanan and G. Karsai. Towards verifying model transformations. In R. Bruni and D. Varr\u00f3, editors, 5th International Workshop on Graph Transformation and Visual Modeling Techniques, Vienna, pages 185--194, Apr 2006.]]"},{"key":"e_1_3_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_109_1","doi-asserted-by":"publisher","DOI":"10.5555\/555142"},{"key":"e_1_3_2_1_110_1","volume-title":"Proceedings of RV'01","author":"Nimmer J. W.","year":"2001","unstructured":"J. W. Nimmer and M. D. Ernst . Static verification of dynamically detected program invariants: Integrating Daikon and ESC\/Java . In Proceedings of RV'01 , First Workshop on Runtime Verification. Elsevier , July 2001 .]] J. W. Nimmer and M. D. Ernst. Static verification of dynamically detected program invariants: Integrating Daikon and ESC\/Java. In Proceedings of RV'01, First Workshop on Runtime Verification. Elsevier, July 2001.]]"},{"key":"e_1_3_2_1_111_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. Paulson , and M. Menzel . Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic , volume 2283 of Lecture Notes in Computer Science . Springer-Verlag , 2002 .]] T. Nipkow, L. Paulson, and M. Menzel. Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer-Verlag, 2002.]]"},{"key":"e_1_3_2_1_112_1","series-title":"NATO Science Series F: Computer and Systems Sciences","first-page":"117","volume-title":"Foundations of Secure Computation","author":"Nipkow T.","year":"2000","unstructured":"T. Nipkow , D. von Oheimb , and C. Pusch . \u03bcJava: Embedding a programming language in a theorem prover . In F. L. Bauer and R. Steinbr\u00fcggen, editors, Foundations of Secure Computation , volume 175 of NATO Science Series F: Computer and Systems Sciences , pages 117 -- 144 . IOS Press , 2000 .]] T. Nipkow, D. von Oheimb, and C. Pusch. \u03bcJava: Embedding a programming language in a theorem prover. In F. L. Bauer and R. Steinbr\u00fcggen, editors, Foundations of Secure Computation, volume 175 of NATO Science Series F: Computer and Systems Sciences, pages 117--144. IOS Press, 2000.]]"},{"key":"e_1_3_2_1_113_1","doi-asserted-by":"crossref","unstructured":"J.\n      Noble J.\n      Vitek and \n      J.\n      Potter\n  . \n  Flexible alias protection\n  . In E. Jul editor ECOOP '98 -- Object-Oriented Programming 12th European Conference Brussels Belgium volume \n  1445\n   of \n  Lecture Notes in Computer Science pages \n  158\n  --\n  185\n  . \n  Springer-Verlag July \n  1998\n  .]]   J. Noble J. Vitek and J. Potter. Flexible alias protection. In E. Jul editor ECOOP '98 -- Object-Oriented Programming 12th European Conference Brussels Belgium volume 1445 of Lecture Notes in Computer Science pages 158--185. Springer-Verlag July 1998.]]","DOI":"10.1007\/BFb0054091"},{"key":"e_1_3_2_1_114_1","volume-title":"Information Processing 83, pages 915--920. Elsevier Science Publishers B.V. (North-Holland), Sept. 1983. Proceedings of the IFIP 9th World Computer Congress","author":"Nordstr\u00f6m B.","unstructured":"B. Nordstr\u00f6m and K. Peterson . Types and specifications. In R. E. A. Mason, editor , Information Processing 83, pages 915--920. Elsevier Science Publishers B.V. (North-Holland), Sept. 1983. Proceedings of the IFIP 9th World Computer Congress , Paris, France.]] B. Nordstr\u00f6m and K. Peterson. Types and specifications. In R. E. A. Mason, editor, Information Processing 83, pages 915--920. Elsevier Science Publishers B.V. (North-Holland), Sept. 1983. Proceedings of the IFIP 9th World Computer Congress, Paris, France.]]"},{"key":"e_1_3_2_1_115_1","series-title":"International Series of Monographs on Computer Science","volume-title":"Programming in Martin-Lof's Type Theory","author":"Nordstr\u00f6m B.","year":"1990","unstructured":"B. Nordstr\u00f6m , K. Peterson , and J. M. Smith . Programming in Martin-Lof's Type Theory , volume 7 of International Series of Monographs on Computer Science . Oxford University Press , New York, NY , 1990 .]] B. Nordstr\u00f6m, K. Peterson, and J. M. Smith. Programming in Martin-Lof's Type Theory, volume 7 of International Series of Monographs on Computer Science. Oxford University Press, New York, NY, 1990.]]"},{"key":"e_1_3_2_1_116_1","doi-asserted-by":"publisher","DOI":"10.1145\/190679.190681"},{"key":"e_1_3_2_1_117_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.345827"},{"key":"e_1_3_2_1_118_1","unstructured":"Rodin Partners. Rodin: Rigorous open development environment for complex systems. http:\/\/rodin.cs.ncl.ac.uk\/ 2006.]]  Rodin Partners. Rodin: Rigorous open development environment for complex systems. http:\/\/rodin.cs.ncl.ac.uk\/ 2006.]]"},{"key":"e_1_3_2_1_119_1","doi-asserted-by":"publisher","DOI":"10.1007\/11531142_24"},{"key":"e_1_3_2_1_120_1","first-page":"59","volume-title":"Workshops in Computing","author":"Rose G.","year":"1992","unstructured":"G. Rose . Object- Z. In S. Stepney , R. Barden , and D. Cooper , editors, Object Orientation in Z , Workshops in Computing , pages 59 -- 77 . Springer-Verlag, Cambridge CB2 1LQ, UK , 1992 .]] G. Rose. Object-Z. In S. Stepney, R. Barden, and D. Cooper, editors, Object Orientation in Z, Workshops in Computing, pages 59--77. Springer-Verlag, Cambridge CB2 1LQ, UK, 1992.]]"},{"key":"e_1_3_2_1_121_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_3_2_1_122_1","volume-title":"A Methodology for Language Development. Allyn and Bacon","author":"Schmidt D. A.","year":"1986","unstructured":"D. A. Schmidt . Denotational Semantics : A Methodology for Language Development. Allyn and Bacon , Inc., Boston, Mass ., 1986 .]] D. A. Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Inc., Boston, Mass., 1986.]]"},{"key":"e_1_3_2_1_123_1","doi-asserted-by":"publisher","DOI":"10.1145\/582095.582099"},{"key":"e_1_3_2_1_124_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5979-4"},{"key":"e_1_3_2_1_125_1","doi-asserted-by":"publisher","DOI":"10.1145\/1028664.1028711"},{"key":"e_1_3_2_1_126_1","doi-asserted-by":"publisher","DOI":"10.1145\/375212.375223"},{"key":"e_1_3_2_1_127_1","doi-asserted-by":"publisher","DOI":"10.5555\/381473.381542"},{"key":"e_1_3_2_1_128_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.585503"},{"key":"e_1_3_2_1_129_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.58788"},{"key":"e_1_3_2_1_130_1","first-page":"251","volume-title":"Proceedings of the NATO Advanced Study Institute","author":"Smith D. R.","year":"1999","unstructured":"D. R. Smith . Mechanizing the development of software. In M. Broy and R. Steinbrueggen, editors, Calculational System Design , Proceedings of the NATO Advanced Study Institute , pages 251 -- 292 . IOS Press, Amsterdam , 1999 .]] D. R. Smith. Mechanizing the development of software. In M. Broy and R. Steinbrueggen, editors, Calculational System Design, Proceedings of the NATO Advanced Study Institute, pages 251--292. IOS Press, Amsterdam, 1999.]]"},{"key":"e_1_3_2_1_131_1","series-title":"International Series in Computer Science","volume-title":"A Reference Manual","author":"Spivey J. M.","year":"1992","unstructured":"J. M. Spivey . The Z Notation : A Reference Manual . International Series in Computer Science . Prentice-Hall , New York, NY , second edition, 1992 .]] J. M. Spivey. The Z Notation: A Reference Manual. International Series in Computer Science. Prentice-Hall, New York, NY, second edition, 1992.]]"},{"key":"e_1_3_2_1_132_1","volume-title":"An electronic purse: Specification, refinement, and proof. Technical monograph PRG-126","author":"Stepney S.","year":"2000","unstructured":"S. Stepney , D. Cooper , and J. Woodcock . An electronic purse: Specification, refinement, and proof. Technical monograph PRG-126 , Oxford University Computing Laboratory , July 2000 .]] S. Stepney, D. Cooper, and J. Woodcock. An electronic purse: Specification, refinement, and proof. Technical monograph PRG-126, Oxford University Computing Laboratory, July 2000.]]"},{"key":"e_1_3_2_1_133_1","series-title":"Lecture Notes in Computer Science","volume-title":"Deductive composition of astronomical software from subroutine libraries","author":"Stickel M. E.","year":"1994","unstructured":"M. E. Stickel , R. Waldinger , M. Lowry , T. Pressburger , and I. Underwood . Deductive composition of astronomical software from subroutine libraries . In A. Bundy, editor, 12th Conference on Automated Deduction, volume 814 of Lecture Notes in Computer Science . Springer-Verlag , 1994 .]] M. E. Stickel, R. Waldinger, M. Lowry, T. Pressburger, and I. Underwood. Deductive composition of astronomical software from subroutine libraries. In A. Bundy, editor, 12th Conference on Automated Deduction, volume 814 of Lecture Notes in Computer Science. Springer-Verlag, 1994.]]"},{"key":"e_1_3_2_1_134_1","volume-title":"Mar.","author":"Stratego","year":"2006","unstructured":"Stratego documentation. http:\/\/tinyurl.com\/nr2c5 , Mar. 2006 .]] Stratego documentation. http:\/\/tinyurl.com\/nr2c5, Mar. 2006.]]"},{"key":"e_1_3_2_1_135_1","first-page":"121","article-title":"A survey of program slicing techniques","volume":"3","author":"Tip F.","year":"1995","unstructured":"F. Tip . A survey of program slicing techniques . Journal of Programming Languages , 3 : 121 -- 189 , 1995 .]] F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3:121--189, 1995.]]","journal-title":"Journal of Programming Languages"},{"key":"e_1_3_2_1_136_1","doi-asserted-by":"publisher","DOI":"10.5555\/645790.667972"},{"key":"e_1_3_2_1_137_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume-title":"T. Margaria and W. Yi","author":"van den Berg J.","year":"2001","unstructured":"J. van den Berg and B. Jacobs . The LOOP compiler for Java and JML . In T. Margaria and W. Yi , editors, Tools and Algorithms for the Construction and Analysis of Software (TACAS), volume 2031 of Lecture Notes in Computer Science , pages 299 -- 312 . Springer-Verlag , 2001 .]] J. van den Berg and B. Jacobs. The LOOP compiler for Java and JML. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Software (TACAS), volume 2031 of Lecture Notes in Computer Science, pages 299--312. Springer-Verlag, 2001.]]"},{"key":"e_1_3_2_1_138_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337184"},{"key":"e_1_3_2_1_139_1","unstructured":"P. Voda. What can we gain by integrating a language processor with a theorem prover. unpublished; available from the author's web site 2003.]]  P. Voda. What can we gain by integrating a language processor with a theorem prover. unpublished; available from the author's web site 2003.]]"},{"key":"e_1_3_2_1_140_1","volume-title":"The Object Constraint Language: Precise Modeling with UML","author":"Warmer J.","year":"1999","unstructured":"J. Warmer and A. Kleppe . The Object Constraint Language: Precise Modeling with UML . Addison Wesley Longman, Reading , Mass ., 1999 .]] J. Warmer and A. Kleppe. The Object Constraint Language: Precise Modeling with UML. Addison Wesley Longman, Reading, Mass., 1999.]]"},{"key":"e_1_3_2_1_141_1","doi-asserted-by":"publisher","DOI":"10.1109\/tse.1984.5010248"},{"key":"e_1_3_2_1_142_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086400"},{"key":"e_1_3_2_1_143_1","doi-asserted-by":"publisher","DOI":"10.1145\/9758.10500"},{"key":"e_1_3_2_1_144_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"e_1_3_2_1_145_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264291"},{"key":"e_1_3_2_1_146_1","first-page":"72","volume-title":"Proceedings of the International Conference on Software Engineering and Formal Methods","author":"Xi H.","year":"2003","unstructured":"H. Xi . Facilitating program verification with dependent types . In Proceedings of the International Conference on Software Engineering and Formal Methods , pages 72 -- 81 , 2003 .]] H. Xi. Facilitating program verification with dependent types. In Proceedings of the International Conference on Software Engineering and Formal Methods, pages 72--81, 2003.]]"},{"key":"e_1_3_2_1_147_1","doi-asserted-by":"publisher","DOI":"10.1145\/237432.237434"}],"event":{"name":"GPCE06: Generative Programming and Component Engineering 2006","location":"Portland Oregon USA","acronym":"GPCE06","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 5th international conference on Generative programming and component engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1173706.1173740","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T02:00:28Z","timestamp":1673229628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1173706.1173740"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10,22]]},"references-count":140,"alternative-id":["10.1145\/1173706.1173740","10.1145\/1173706"],"URL":"https:\/\/doi.org\/10.1145\/1173706.1173740","relation":{},"subject":[],"published":{"date-parts":[[2006,10,22]]},"assertion":[{"value":"2006-10-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}