{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,22]],"date-time":"2023-08-22T13:21:17Z","timestamp":1692710477958},"reference-count":30,"publisher":"Elsevier BV","issue":"3-4","license":[{"start":{"date-parts":[[1991,1,1]],"date-time":"1991-01-01T00:00:00Z","timestamp":662688000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computer Languages"],"published-print":{"date-parts":[[1991,1]]},"DOI":"10.1016\/0096-0551(91)90010-7","type":"journal-article","created":{"date-parts":[[2003,8,7]],"date-time":"2003-08-07T19:04:53Z","timestamp":1060283093000},"page":"259-280","source":"Crossref","is-referenced-by-count":7,"title":["Modular verification of Ada generics"],"prefix":"10.1016","volume":"16","author":[{"given":"George W","family":"Ernst","sequence":"first","affiliation":[]},{"given":"Raymond J","family":"Hookway","sequence":"additional","affiliation":[]},{"given":"James A","family":"Menegay","sequence":"additional","affiliation":[]},{"given":"William F","family":"Ogden","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0096-0551(91)90010-7_BIB1","series-title":"Reference Manual for the Ada Programming Language","year":"1983"},{"key":"10.1016\/0096-0551(91)90010-7_BIB2","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","article-title":"Soundness and completeness of an axiom system for program verification","author":"Cook","year":"1978","journal-title":"SIAM J. Comput."},{"key":"10.1016\/0096-0551(91)90010-7_BIB3","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/322108.322121","article-title":"Programming language constructs for which it is impossible to obtain good Hoare axiom systems","author":"Clarke","year":"1979","journal-title":"J. ACM"},{"key":"10.1016\/0096-0551(91)90010-7_BIB4","series-title":"Behavioral equivalence relations induced by programming logics","author":"Brookes","year":"1983"},{"key":"10.1016\/0096-0551(91)90010-7_BIB5","doi-asserted-by":"crossref","DOI":"10.1007\/BF00264436","article-title":"Verification of procedures with procedure-type parameters","author":"Ernst","year":"1982","journal-title":"Acta inform."},{"key":"10.1016\/0096-0551(91)90010-7_BIB6","series-title":"VERkshop III\u2014a formal verification workshop proceedings","year":"1985"},{"key":"10.1016\/0096-0551(91)90010-7_BIB7","series-title":"Proc. of the ACM\u2014SIGPLAN Symposium on the Ada Programming Language","article-title":"Generics and verification in Ada","author":"Young","year":"1980"},{"key":"10.1016\/0096-0551(91)90010-7_BIB8","series-title":"Symposium on Principles of Programming Languages","first-page":"322","article-title":"Modular verification of concurrent programs","author":"Hailpern","year":"1982"},{"key":"10.1016\/0096-0551(91)90010-7_BIB9","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/BF00261258","article-title":"Sound and complete Hoare-like calculi based on copy rules","volume":"16","author":"Olderog","year":"1981","journal-title":"Acta inform."},{"key":"10.1016\/0096-0551(91)90010-7_BIB10","article-title":"Semantics of programming languages for modular verification","author":"Ernst","year":"1985"},{"key":"10.1016\/0096-0551(91)90010-7_BIB11","article-title":"Complementary definitions of programming language semantics","author":"Donahue","year":"1975"},{"key":"10.1016\/0096-0551(91)90010-7_BIB12","article-title":"A complete axiomatic system for proving assertions about recursive and non-recursive programs","author":"Gorelick","year":"1975"},{"key":"10.1016\/0096-0551(91)90010-7_BIB13","series-title":"Principles of Programming Languages Conf. Record","first-page":"262","article-title":"A good Hoare axiom system for an algol-like language","author":"Halpern","year":"1984"},{"key":"10.1016\/0096-0551(91)90010-7_BIB14","series-title":"Principles of Programming Languages Conf. Record","first-page":"245","article-title":"The semantics of local storage, or what makes the fre-list free?","author":"Halpern","year":"1984"},{"key":"10.1016\/0096-0551(91)90010-7_BIB15","series-title":"Proc. of Logics of Programs","article-title":"Reasoning about procedures as parameters","author":"German","year":"1983"},{"key":"10.1016\/0096-0551(91)90010-7_BIB16","article-title":"An extended semantic definition of Pascal for probing the absence of common runtime errors","author":"German","year":"1980"},{"key":"10.1016\/0096-0551(91)90010-7_BIB17","article-title":"ANNA A Language for Annotating Ada Programs","volume":"260","author":"Luckham","year":"1987"},{"key":"10.1016\/0096-0551(91)90010-7_BIB18","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/BF00264295","article-title":"A sound and relatively complete Hoare-logic for a language with higher type procedure","volume":"20","author":"Damm","year":"1983","journal-title":"Acta inform."},{"key":"10.1016\/0096-0551(91)90010-7_BIB19","series-title":"Proc. of Specification of Reliable Software","first-page":"170","article-title":"An introduction to OBJ-T","author":"Goguen","year":"1979"},{"key":"10.1016\/0096-0551(91)90010-7_BIB20","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/BF00289507","article-title":"Proof of correctness of data representations","author":"Hoare","year":"1972","journal-title":"Acta inform."},{"key":"10.1016\/0096-0551(91)90010-7_BIB21","series-title":"Verification Assessment Study, Final Report, Vol. II, The Gypsy System","first-page":"49","article-title":"A critique of the gypsy verification system","author":"Kemmerer","year":"1986"},{"key":"10.1016\/0096-0551(91)90010-7_BIB22","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1145\/357114.357117","article-title":"Specification of abstract data types in Modula","author":"Ernst","year":"1980","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"10.1016\/0096-0551(91)90010-7_BIB23","series-title":"Verification Assessment Study, Final Report, Vol. III, The AFFIRM\u00b7System","first-page":"21","article-title":"AFFIRM review","author":"Cooper","year":"1986"},{"key":"10.1016\/0096-0551(91)90010-7_BIB24","series-title":"Data Structures and Algorithms","author":"Aho","year":"1983"},{"key":"10.1016\/0096-0551(91)90010-7_BIB25","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","author":"Hoare","year":"1969","journal-title":"Commun. ACM"},{"key":"10.1016\/0096-0551(91)90010-7_BIB26","series-title":"Computers and Automation","first-page":"19","article-title":"Toward a methematical semantics for computer languages","author":"Scott","year":"1972"},{"key":"10.1016\/0096-0551(91)90010-7_BIB27","series-title":"Introduction to Metamathematics","author":"Kleene","year":"1952"},{"key":"10.1016\/0096-0551(91)90010-7_BIB28","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0022-0000(67)80014-X","article-title":"Some definitional suggestions for automata theory","volume":"1","author":"Scott","year":"1967","journal-title":"J. Comput. Syst. Sci."},{"key":"10.1016\/0096-0551(91)90010-7_BIB29","series-title":"Continuous Model Theory","author":"Chang","year":"1966"},{"key":"10.1016\/0096-0551(91)90010-7_BIB30","series-title":"Uniform specification of a diverse collection of abstract data types","author":"Ogden","year":"1987"}],"container-title":["Computer Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0096055191900107?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0096055191900107?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T03:25:05Z","timestamp":1552620305000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0096055191900107"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,1]]},"references-count":30,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[1991,1]]}},"alternative-id":["0096055191900107"],"URL":"https:\/\/doi.org\/10.1016\/0096-0551(91)90010-7","relation":{},"ISSN":["0096-0551"],"issn-type":[{"value":"0096-0551","type":"print"}],"subject":[],"published":{"date-parts":[[1991,1]]}}}