{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:47:17Z","timestamp":1725893237050},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540773948"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-77395-5_1","type":"book-chapter","created":{"date-parts":[[2007,12,6]],"date-time":"2007-12-06T11:25:53Z","timestamp":1196940353000},"page":"1-8","source":"Crossref","is-referenced-by-count":3,"title":["PSL for Runtime Verification: Theory and Practice"],"prefix":"10.1007","author":[{"given":"Cindy","family":"Eisner","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_40","volume-title":"Proc. 12 th International Conference on Computer Aided Verification (CAV)","author":"Y. Abarbanel","year":"2000","unstructured":"Abarbanel, Y., Beer, I., Gluhovsky, L., Keidar, S., Wolfsthal, Y.: FoCs - automatic generation of simulation checkers from formal specifications. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"1_CR2","unstructured":"Accellera property specification language reference manual, http:\/\/www.eda.org\/vfv\/docs\/psl_lrm-1.1.pdf"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2003","unstructured":"Armoni, R., Bustan, D., Kupferman, O., Vardi, M.Y.: Aborts vs resets in linear temporal logic. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, Springer, Heidelberg (2003)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Barner, S., Glazberg, Z., Rabinovitz, I.: Wolf - bug hunter for concurrent software using formal methods. In: CAV, pp. 153\u2013157 (2005)","DOI":"10.1007\/11513988_16"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","first-page":"14","volume-title":"First International Haifa Verification Conference","author":"S. Ben-David","year":"2005","unstructured":"Ben-David, S., Fisman, D., Ruah, S.: The safety simple subset. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) First International Haifa Verification Conference. LNCS, vol.\u00a03875, pp. 14\u201329. Springer, Heidelberg (2005)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Proc. 5 th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, Springer, Heidelberg (1999)"},{"key":"1_CR7","unstructured":"Cheung, P.H., Forin, A.: A C-language binding for PSL. In: Technical Report MSR-TR-2006-131, Microsoft Research (2006)"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E. Clarke","year":"1982","unstructured":"Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Dahan, A., Geist, D., Gluhovsky, L., Pidan, D., Shapir, G., Wolfsthal, Y., Benalycherif, L., Kamdem, R., Lahbib, Y.: Combining system level modeling with assertion based verification. In: ISQED, pp. 310\u2013315 (2005)","DOI":"10.1109\/ISQED.2005.32"},{"key":"1_CR10","volume-title":"Electronic Notes in Theoretical Computer Science","author":"C. Eisner","year":"2001","unstructured":"Eisner, C.: Model checking the garbage collection mechanism of SMV. In: Stoller, S.D., Visser, W. (eds.) Electronic Notes in Theoretical Computer Science, vol.\u00a055, Elsevier, Amsterdam (2001)"},{"issue":"1","key":"1_CR11","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/s10270-003-0042-x","volume":"4","author":"C. Eisner","year":"2005","unstructured":"Eisner, C.: Formal verification of software source code through semi-automatic modeling. Software and Systems Modeling\u00a04(1), 14\u201331 (2005)","journal-title":"Software and Systems Modeling"},{"key":"1_CR12","volume-title":"A Practical Introduction to PSL","author":"C. Eisner","year":"2006","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Eisner, C., Fisman, D., Havlicek, J.: A topological characterization of weakness. In: Proc. 24th Annual ACM Symposium on Principles of Distributed Com puting (PODC), pp. 1\u20138 (2005)","DOI":"10.1145\/1073814.1073816"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/978-3-540-45069-6_3","volume-title":"Computer Aided Verification","author":"C. Eisner","year":"2003","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 27\u201339. Springer, Heidelberg (2003)"},{"key":"1_CR15","unstructured":"Eisner, C., Fisman, D., Havlicek, J., M\u00e5rtensson, J.: The \u22a4, $\\bot$ approach for truncated semantics. Technical Report 2006.01, Accellera (January 2006)"},{"key":"1_CR16","unstructured":"IEEE standard for property specification language (PSL). IEEE Std 1850-2005"},{"key":"1_CR17","volume-title":"Proc. 41st Annual Symposium on Foundations of Computer Science","author":"M. Maidl","year":"2000","unstructured":"Maidl, M.: The common fragment of CTL and LTL. In: Proc. 41st Annual Symposium on Foundations of Computer Science, IEEE, Los Alamitos (November 2000)"},{"key":"1_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)"},{"key":"1_CR19","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"Pnueli, A.: A temporal logic of concurrent programs. Theoretical Computer Science\u00a013, 45\u201360 (1981)","journal-title":"Theoretical Computer Science"},{"key":"1_CR20","unstructured":"RuleBase. Available from the IBM Haifa Research Laboratory, See http:\/\/www.haifa.il.ibm.com\/projects\/verification\/RB_Homepage\/"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45319-9_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.Y. Vardi","year":"2001","unstructured":"Vardi, M.Y.: Branching vs. linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 1\u201322. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-77395-5_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:10:30Z","timestamp":1619521830000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77395-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540773948"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77395-5_1","relation":{},"subject":[]}}