{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T06:42:25Z","timestamp":1726036945767},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030255398"},{"type":"electronic","value":"9783030255404"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-25540-4_32","type":"book-chapter","created":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T15:02:35Z","timestamp":1562943755000},"page":"553-571","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Local and Compositional Reasoning for Optimized Reactive Systems"],"prefix":"10.1007","author":[{"given":"Mitesh","family":"Jain","sequence":"first","affiliation":[]},{"given":"Panagiotis","family":"Manolios","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,12]]},"reference":[{"key":"32_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/3-540-44798-9_33","volume-title":"Correct Hardware Design and Verification Methods","author":"MD Aagaard","year":"2001","unstructured":"Aagaard, M.D., Cook, B., Day, N.A., Jones, R.B.: A framework for microprocessor correctness statements. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 433\u2013448. Springer, Heidelberg (2001). \n                      https:\/\/doi.org\/10.1007\/3-540-44798-9_33"},{"key":"32_CR2","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0020-0190(96)00034-8","volume":"58","author":"T Basten","year":"1996","unstructured":"Basten, T.: Branching bisimilarity is an equivalence indeed!. Inf. Process. Lett. 58, 141\u2013147 (1996)","journal-title":"Inf. Process. Lett."},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-19835-9_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"HR Chamarthi","year":"2011","unstructured":"Chamarthi, H.R., Dillinger, P., Manolios, P., Vroon, D.: The ACL2 sedan theorem proving system. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 291\u2013295. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-19835-9_27"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state processes. In: PODC (1986)","DOI":"10.21236\/ADA188743"},{"key":"32_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/BFb0039066","volume-title":"CONCUR \u201990 Theories of Concurrency: Unification and Extension","author":"RJ Glabbeek van","year":"1990","unstructured":"van Glabbeek, R.J.: The linear time-branching time spectrum (extended abstract). In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278\u2013297. Springer, Heidelberg (1990). \n                      https:\/\/doi.org\/10.1007\/BFb0039066"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Gu, L., Vaynberg, A., Ford, B., Shao, Z., Costanzo, D.: CertiKOS: a certified kernel for secure cloud computing. In: APSys (2011)","DOI":"10.1145\/2103799.2103803"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Gu, R., et al.: Deep specifications and certified abstraction layers. In: POPL (2015)","DOI":"10.1145\/2676726.2676975"},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., et al.: IronFleet: Proving practical distributed systems correct. In: SOSP (2015)","DOI":"10.1145\/2815400.2815428"},{"key":"32_CR9","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1024716316140","volume":"23","author":"R Hosabettu","year":"2003","unstructured":"Hosabettu, R., Gopalakrishnan, G., Srivas, M.: Formal verification of a complex pipelined processor. Form. Methods Syst. Des. 23, 171\u2013213 (2003)","journal-title":"Form. Methods Syst. Des."},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-319-21690-4_7","volume-title":"Computer Aided Verification","author":"M Jain","year":"2015","unstructured":"Jain, M., Manolios, P.: Skipping refinement. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 103\u2013119. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-21690-4_7"},{"key":"32_CR11","unstructured":"Klarlund, N.: Progress measures and finite arguments for infinite computations. Ph.D. thesis (1990)"},{"key":"32_CR12","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-1-4419-1539-9_11","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"G Klein","year":"2010","unstructured":"Klein, G., Sewell, T., Winwood, S.: Refinement in the formal verification of the seL4 microkernel. In: Hardin, D. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 323\u2013339. Springer, Boston (2010). \n                      https:\/\/doi.org\/10.1007\/978-1-4419-1539-9_11"},{"key":"32_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-319-96145-3_5","volume-title":"Computer Aided Verification","author":"B Kragl","year":"2018","unstructured":"Kragl, B., Qadeer, S.: Layered concurrent programs. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 79\u2013102. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-96145-3_5"},{"key":"32_CR14","unstructured":"Lamport, L.: What good is temporal logic. Information processing (1993)"},{"key":"32_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal verification of a c-like memory model and its uses for verifying program transformations. J. Autom. Reason. 41, 1\u201331 (2008)","journal-title":"J. Autom. Reason."},{"key":"32_CR16","doi-asserted-by":"crossref","unstructured":"Liu, X., Yu, T., Zhang, W.: Analyzing divergence in bisimulation semantics. In: POPL (2017)","DOI":"10.1145\/3009837.3009870"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations: I. Untimed systems. Inf. Comput. (1995)","DOI":"10.1006\/inco.1995.1134"},{"key":"32_CR18","unstructured":"Manolios, P.: Mechanical verification of reactive systems. Ph.D. thesis, University of Texas (2001)"},{"key":"32_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-40922-X_11","volume-title":"Formal Methods in Computer-Aided Design","author":"P Manolios","year":"2000","unstructured":"Manolios, P.: Correctness of pipelined machines. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 181\u2013198. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/3-540-40922-X_11"},{"key":"32_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-540-39724-3_28","volume-title":"Correct Hardware Design and Verification Methods","author":"P Manolios","year":"2003","unstructured":"Manolios, P.: A compositional theory of refinement for branching time. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 304\u2013318. Springer, Heidelberg (2003). \n                      https:\/\/doi.org\/10.1007\/978-3-540-39724-3_28"},{"key":"32_CR21","unstructured":"Manolios, P., Srinivasan, S.K.: A complete compositional reasoning framework for the efficient verification of pipelined machines. In: ICCAD (2005)"},{"key":"32_CR22","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Proceedings of the 2nd International Joint Conference on Artificial Intelligence (1971)"},{"key":"32_CR23","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/6462.6485","volume":"18","author":"J Misra","year":"1986","unstructured":"Misra, J.: Distributed discrete-event simulation. ACM Comput. Surv. 18, 39\u201365 (1986)","journal-title":"ACM Comput. Surv."},{"key":"32_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/BFb0058037","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"KS Namjoshi","year":"1997","unstructured":"Namjoshi, K.S.: A simple characterization of stuttering bisimulation. In: Ramesh, S., Sivakumar, G. (eds.) FSTTCS 1997. LNCS, vol. 1346, pp. 284\u2013296. Springer, Heidelberg (1997). \n                      https:\/\/doi.org\/10.1007\/BFb0058037"},{"key":"32_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-38856-9_17","volume-title":"Static Analysis","author":"KS Namjoshi","year":"2013","unstructured":"Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 304\u2013323. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-38856-9_17"},{"key":"32_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-540-27813-9_3","volume-title":"Computer Aided Verification","author":"S Ray","year":"2004","unstructured":"Ray, S., Jr Hunt, W.A.: Deductive verification of pipelined machines using first-order quantification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 31\u201343. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-27813-9_3"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-25540-4_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T15:07:04Z","timestamp":1562944024000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-25540-4_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030255398","9783030255404"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-25540-4_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New York City, NY","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav0","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"258","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}