{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:37:30Z","timestamp":1725557850582},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540201755"},{"type":"electronic","value":"9783540399797"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"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":[[2003]]},"DOI":"10.1007\/978-3-540-39979-7_9","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T14:52:22Z","timestamp":1277218342000},"page":"127-143","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Verification of Annotated Code"],"prefix":"10.1007","author":[{"given":"Doron","family":"Peled","sequence":"first","affiliation":[]},{"given":"Hongyang","family":"Qu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4376-0","volume-title":"Verification of Sequential and Concurrent Programs","author":"K.R. Apt","year":"1991","unstructured":"Apt, K.R., Olderog, E.R.: Verification of Sequential and Concurrent Programs. Springer, Heidelberg (1991)"},{"key":"9_CR2","volume-title":"Principles of Concurrent and Distributed Programming","author":"M. Ben Ari","year":"1990","unstructured":"Ben Ari, M.: Principles of Concurrent and Distributed Programming. Prentice Hall, Englewood Cliffs (1990)"},{"key":"9_CR3","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BFb0028741","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"1988","unstructured":"Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 147\u2013158. Springer, Heidelberg (1988)"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Communications of the ACM\u00a018, 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-46017-9_18","volume-title":"Model Checking Software","author":"C. Eisner","year":"2002","unstructured":"Eisner, C., Peled, D.: Comparing Symbolic and Explicit Model Checking of a Software Systems. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 230\u2013239. Springer, Heidelberg (2002)"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Evans, D., Guttag, J., Horning, J., Tan, Y.M.: LCLint: A tool for using specifications to check code. In: Proceedings of the SIGSOFT symposium on the foundations of software engineering, pp. 87\u201396 (1994)","DOI":"10.1145\/193173.195297"},{"key":"9_CR8","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. In: PLDI 2002, pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"9_CR9","volume-title":"Program Verification","author":"N. Francez","year":"1992","unstructured":"Francez, N.: Program Verification. Addison-Wesley, Reading (1992)"},{"key":"9_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4886-6","volume-title":"Fairness","author":"N. Francez","year":"1986","unstructured":"Francez, N.: Fairness. Springer, Heidelberg (1986)"},{"key":"9_CR11","volume-title":"The Spin Model Checker, Primer and Reference Manual","author":"G. Holzmann","year":"2003","unstructured":"Holzmann, G.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003) (to appear)"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D.: An improvement inFormal Verification. In: FORTE 1994, pp. 197\u2013211 (1994)","DOI":"10.1007\/978-0-387-34878-0_13"},{"key":"9_CR13","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/0304-3975(92)90054-J","volume":"101","author":"S. Katz","year":"1992","unstructured":"Katz, S., Peled, D.: Defining conditional independence using collapses. Theoretical Computer Science\u00a0101, 337\u2013359 (1992)","journal-title":"Theoretical Computer Science"},{"key":"9_CR14","doi-asserted-by":"publisher","DOI":"10.1515\/9781400864041","volume-title":"Computer-Aided Verification of Coordinating Processes","author":"R. Kurshan","year":"1995","unstructured":"Kurshan, R.: Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1995)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/3-540-44618-4_41","volume-title":"CONCUR 2000 - Concurrency Theory","author":"R. Lazic","year":"2002","unstructured":"Lazic, R., Nowak, D.: A unifying approach to data-independence. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 581\u2013595. Springer, Heidelberg (2002)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. Software Tools for Technology Transfer (to appear)","DOI":"10.1007\/s10009-002-0104-3"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: How to cook a temporal proof system for your pet language. In: Principles of Programming Languages, Austin, Texas, pp. 167\u2013176 (1983)","DOI":"10.1145\/567067.567082"},{"key":"9_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"9_CR19","volume-title":"The Art of Software Testing","author":"G.J. Myers","year":"1979","unstructured":"Myers, G.J.: The Art of Software Testing. Wiley, Chichester (1979)"},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S. Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. CACM\u00a019, 279\u2013285 (1976)","journal-title":"CACM"},{"key":"9_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3540-6","volume-title":"Software Reliability Methods","author":"D.A. Peled","year":"2001","unstructured":"Peled, D.A.: Software Reliability Methods. Springer, Heidelberg (2001)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th IEEE symposium on Foundation of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: Principles of Programming Languages, St. Petersburg Beach, Fl, pp. 184\u2013193 (1986)","DOI":"10.1145\/512644.512661"},{"key":"9_CR24","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st Annual Symposium on Logic in Computer Science IEEE, pp. 332\u2013344 (1986)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Systems - FORTE 2003"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39979-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T05:36:13Z","timestamp":1559194573000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39979-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540201755","9783540399797"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39979-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}