{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,13]],"date-time":"2023-01-13T19:32:24Z","timestamp":1673638344735},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2007,6,6]],"date-time":"2007-06-06T00:00:00Z","timestamp":1181088000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2008,7]]},"DOI":"10.1007\/s10270-007-0060-1","type":"journal-article","created":{"date-parts":[[2007,6,5]],"date-time":"2007-06-05T12:01:24Z","timestamp":1181044884000},"page":"257-272","source":"Crossref","is-referenced-by-count":1,"title":["Flexible and configurable verification policies with Omnibus"],"prefix":"10.1007","volume":"7","author":[{"given":"Thomas","family":"Wilson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Savi","family":"Maharaj","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert G.","family":"Clark","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,6,6]]},"reference":[{"key":"60_CR1","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. Proceedings of CASSIS 2004, Springer, Heidelberg, LNCS 3362 (2004)"},{"key":"60_CR2","doi-asserted-by":"crossref","unstructured":"Chalin, P.: Logical foundations of program assertions: what do practitioners want?. Proceedings of SEFM 2005, IEEE Computer Society (2004)","DOI":"10.1109\/SEFM.2005.26"},{"key":"60_CR3","doi-asserted-by":"crossref","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: Uniting ESC\/Java and JML: Progress and issues in building and using ESC\/Java2. NIII technical report R0413 (2004)","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"60_CR4","doi-asserted-by":"crossref","unstructured":"Crocker, D.: Safe object-oriented software: the verified design-by-contract paradigm. Proceedings of the 12th safety-critical systems symposium, Springer, Heidelberg (2004)","DOI":"10.1007\/978-0-85729-408-1_2"},{"key":"60_CR5","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (2003)"},{"key":"60_CR6","doi-asserted-by":"crossref","unstructured":"Dietl, W., M\u00fcller, P.: Universes: lightweight ownership for JML. J. Object Technol. 4(8), (2005)","DOI":"10.5381\/jot.2005.4.8.a1"},{"key":"60_CR7","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. Proceedings of PLDI 2002, ACM SIGPLAN Notices 37(5) (2002)","DOI":"10.1145\/543552.512558"},{"key":"60_CR8","doi-asserted-by":"crossref","unstructured":"Jacobs, B., March\u00e9, C., Rauch, N.: Formal verification of a commercial smart card applet with multiple tools. Proceedings of AMAST 2004, Springer, Heidelberg, LNCS 3116 (2004)","DOI":"10.1007\/978-3-540-27815-3_21"},{"key":"60_CR9","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary Design of JML: A behavioral interface specification language for Java. Department of Computer Science, Iowa State University, TR#98\u201306p (2003)"},{"key":"60_CR10","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Extended static checking: a ten-year perspective. Informatics\u201410\u00a0years back, 10\u00a0years ahead, Springer LNCS 2000 (2001)","DOI":"10.1007\/3-540-44577-3_11"},{"key":"60_CR11","unstructured":"Meyer, B.: Contracts for components. Software Development Magazine, July (2000)"},{"key":"60_CR12","unstructured":"Meyer, B.: Eiffel: The language. ISBN 0132479257, Prentice Hall (2000)"},{"key":"60_CR13","doi-asserted-by":"crossref","unstructured":"Meyer, B.: On to components. IEEE Computer, January (1999)","DOI":"10.1109\/2.738312"},{"key":"60_CR14","doi-asserted-by":"crossref","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: PVS: Combining specification, proof checking, and model checking. Proceedings of CAV 1996, Springer, Heidelberg, LNCS 1102 (1996)","DOI":"10.1007\/3-540-61474-5_91"},{"key":"60_CR15","volume-title":"Kernels for safety?. Safe and secure computing systems","author":"J. Rushby","year":"1989","unstructured":"Rushby J. (1989) Kernels for safety?. Safe and secure computing systems. Blackwell, Oxford"},{"key":"60_CR16","unstructured":"Wilson, T.: Omnibus home page. Available at http:\/\/www.cs.stir.ac.uk\/omnibus\/ (2007)"},{"key":"60_CR17","unstructured":"Wilson, T., Maharaj, S., Clark, R.G.: Push-button tools for software developers, full formal verification for component vendors, Technical Report CSM-167, Department of Computing Science and Mathematics, University of Stirling (2006)"},{"key":"60_CR18","unstructured":"Wilson, T., Maharaj, S., Clark, R.G.: Omnibus: a clean language and supporting tool for integrating different assertion-based verification techniques. Proceedings of the Workshop on Rigorous Engineering of Fault Tolerant Systems (REFT) (2005)"},{"key":"60_CR19","doi-asserted-by":"crossref","unstructured":"Wilson, T., Maharaj, S., Clark, R.G.: Omnibus Verification Policies: a flexible, configurable approach to assertion-based software verification. Proceedings of SEFM 2005, IEEE Computer Society (2005)","DOI":"10.1109\/SEFM.2005.29"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-007-0060-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-007-0060-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-007-0060-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:55:24Z","timestamp":1559116524000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-007-0060-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6,6]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["60"],"URL":"https:\/\/doi.org\/10.1007\/s10270-007-0060-1","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,6,6]]}}}