{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T04:46:12Z","timestamp":1746679572721,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642142949"},{"type":"electronic","value":"9783642142956"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_18","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:36:09Z","timestamp":1278628569000},"page":"171-174","source":"Crossref","is-referenced-by-count":62,"title":["Jtlv: A Framework for Developing Verification Algorithms"],"prefix":"10.1007","author":[{"given":"Amir","family":"Pnueli","sequence":"first","affiliation":[]},{"given":"Yaniv","family":"Sa\u2019ar","sequence":"additional","affiliation":[]},{"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11513988_39","volume-title":"Computer Aided Verification","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Fang, Y., Pnueli, A., Zuck, L.D.: IIV: An Invisible Invariant Verifier. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 408\u2013412. Springer, Heidelberg (2005)"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-70545-1_15","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2008","unstructured":"Cohen, A., Namjoshi, K.S.: Local proofs for linear-time properties of concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 149\u2013161. Springer, Heidelberg (2008)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1007\/978-3-642-14295-6_46","volume-title":"CAV 2010","author":"A. Cohen","year":"2010","unstructured":"Cohen, A., Namjoshi, K.S., Sa\u2019ar, Y.: A dash of fairness for compositional reasoning. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 543\u2013557. Springer, Heidelberg (2010)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"558","DOI":"10.1007\/978-3-642-14295-6_47","volume-title":"CAV 2010","author":"A. Cohen","year":"2010","unstructured":"Cohen, A., Namjoshi, K.S., Sa\u2019ar, Y.: Split: A compositional Ltl verifier. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 558\u2013561. Springer, Heidelberg (2010)"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Cohen, A., Namjoshi, K.S., Sa\u2019ar, Y., Zuck, L.D., Kisyova, K.I.: Parallelizing a symbolic compositional model-checking algorithm (in preparation) (2010)","DOI":"10.1007\/978-3-642-19583-9_9"},{"key":"18_CR7","unstructured":"Gazit, H.K., Ayanian, N., Pappas, G., Kumar, V.: Recycling controllers. In: IEEE Conference on Automation Science and Engineering, Washington (August 2008)"},{"key":"18_CR8","unstructured":"Harel, D., Maoz, S., Segall, I.: Using automata representations of LSCs for smart play-out and synthesis (in preparation) (2010)"},{"key":"18_CR9","unstructured":"Harel, D., Segall, I.: Synthesis from live sequence chart specifications (in preparation) (2010)"},{"key":"18_CR10","volume-title":"Spin model checker, the: primer and reference manual","author":"G. Holzmann","year":"2003","unstructured":"Holzmann, G.: Spin model checker, the: primer and reference manual. Addison-Wesley Professional, Reading (2003)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-540-45069-6_36","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"2003","unstructured":"Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace inclusion. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 381\u2013392. Springer, Heidelberg (2003)"},{"key":"18_CR12","unstructured":"Kesten, Y., Pnueli, A., Raviv, L., Shahar, E.: LTL model checking with strong fairness. Formal Methods in System Design (2002)"},{"key":"18_CR13","unstructured":"Cadence\u00a0Berkeley Lab. Cadence SMV (1998), http:\/\/www-cad.eecs.berkeley.edu\/kenmcmil\/smv"},{"key":"18_CR14","unstructured":"Nielson, J.L.: Buddy, http:\/\/buddy.sourceforge.net"},{"key":"18_CR15","unstructured":"Piterman, N.: Suggested projects (2009), http:\/\/www.doc.ic.ac.uk\/~npiterma\/projects.html"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A.: Faster solutions of rabin and streett games. In: LICS, pp. 275\u2013284 (2006)","DOI":"10.1109\/LICS.2006.23"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Piterman","year":"2005","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-61474-5_68","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"1996","unstructured":"Pnueli, A., Shahar, E.: A platform for combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 184\u2013195. Springer, Heidelberg (1996)"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Ranjan, R.K., Sanghavi, J.V., Brayton, R.K., Vincentelli, A.S.: High performance BDD package based on exploiting memory hierarchy. In: DAC\u201996, June 1996, pp. 635\u2013640 (1996)","DOI":"10.1145\/240518.240638"},{"key":"18_CR20","unstructured":"Sa\u2019ar, Y.: JTLV \u2013 web API, http:\/\/jtlv.ysaar.net\/resources\/javaDoc\/API1.3.2\/"},{"key":"18_CR21","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram package (1998), http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"},{"key":"18_CR22","unstructured":"Whaley, J.: JavaBDD, http:\/\/javabdd.sourceforge.net"},{"key":"18_CR23","unstructured":"Wongpiromsarn, T., Topcu, U., Murray, R.M.: Automatic synthesis of robust embedded control software. submitted to AAAI\u201910 (2010)"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon control for temporal logic specifications. In: HSCC\u201910 (2010)","DOI":"10.1145\/1755952.1755968"}],"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-642-14295-6_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T19:49:15Z","timestamp":1740253755000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}