{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T09:28:39Z","timestamp":1780565319978,"version":"3.54.1"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2012,1,19]],"date-time":"2012-01-19T00:00:00Z","timestamp":1326931200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2012,12]]},"DOI":"10.1007\/s10703-011-0139-8","type":"journal-article","created":{"date-parts":[[2012,1,18]],"date-time":"2012-01-18T16:52:44Z","timestamp":1326905564000},"page":"236-268","source":"Crossref","is-referenced-by-count":33,"title":["Optimized temporal monitors for SystemC"],"prefix":"10.1007","volume":"41","author":[{"given":"Deian","family":"Tabakov","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kristin Y.","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2012,1,19]]},"reference":[{"key":"139_CR1","doi-asserted-by":"crossref","first-page":"538","DOI":"10.1007\/10722167_40","volume-title":"CAV\u201900: Proc of the 12th international conference on computer aided verification","author":"Y Abarbanel","year":"2000","unstructured":"Abarbanel Y, Beer I, Gluhovsky L, Keidar S, Wolfsthal Y (2000) Focs: Automatic generation of simulation checkers from formal specifications. In: CAV\u201900: Proc of the 12th international conference on computer aided verification, pp 538\u2013542"},{"key":"139_CR2","series-title":"LNCS","volume-title":"Proc workshop on formal approaches to testing and runtime verification","author":"R Armoni","year":"2006","unstructured":"Armoni R, Korchemny D, Tiemeyer A, Vardi M, Zbar Y (2006) Deterministic dynamic monitors for linear-time assertions. In: Proc workshop on formal approaches to testing and runtime verification. LNCS, vol\u00a04262. Springer, Berlin"},{"key":"139_CR3","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/11944836_25","volume-title":"FSTTCS\u201906: Foundations of software technology and theoretical computer science, 26th international conference","author":"A Bauer","year":"2006","unstructured":"Bauer A, Leucker M, Schallhart C (2006) Monitoring of real-time properties. In: FSTTCS\u201906: Foundations of software technology and theoretical computer science, 26th international conference. LNCS, vol\u00a04337. Springer, Berlin, pp 260\u2013272"},{"issue":"3","key":"139_CR4","doi-asserted-by":"crossref","first-page":"707","DOI":"10.1093\/logcom\/exn077","volume":"20","author":"E Bodden","year":"2010","unstructured":"Bodden E, Hendren LJ, Lam P, Lhot\u00e1k O, Naeem NA (2010) Collaborative runtime verification with tracematches. J Log Comput 20(3):707\u2013723","journal-title":"J Log Comput"},{"key":"139_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4020-8586-4","volume-title":"Generating hardware assertion checkers","author":"M Boul\u00e9","year":"2008","unstructured":"Boul\u00e9 M, Zilic Z (2008) Generating hardware assertion checkers. Springer, Berlin"},{"key":"139_CR6","doi-asserted-by":"crossref","unstructured":"Bryant R (1986) Graph-based algorithms for Boolean-function manipulation. IEEE Trans Comput C-35(8)","DOI":"10.1109\/TC.1986.1676819"},{"issue":"3","key":"139_CR7","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R Bryant","year":"1992","unstructured":"Bryant R (1992) Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293\u2013318","journal-title":"ACM Comput Surv"},{"issue":"1","key":"139_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/966137.966138","volume":"9","author":"A Bunker","year":"2004","unstructured":"Bunker A, Gopalakrishnan G, McKee SA (2004) Formal hardware specification languages for protocol compliance verification. ACM Trans Des Autom Electron Syst 9(1):1\u201332","journal-title":"ACM Trans Des Autom Electron Syst"},{"key":"139_CR9","unstructured":"Bustan D, Fisman D, Havlicek J (2005) Automata construction for PSL. Tech Rep, The Weizmann Institute of Science"},{"key":"139_CR10","volume-title":"Surviving the SOC revolution: a\u00a0guide to platform-based design","author":"H Chang","year":"1999","unstructured":"Chang H, Cooke L, Hunt M, Martin G, McNelly AJ, Todd L (1999) Surviving the SOC revolution: a\u00a0guide to platform-based design. Kluwer Academic, Norwell"},{"key":"139_CR11","first-page":"72","volume-title":"Proceedings of the fourth international conference on intelligent computing and information systems (ICICIS\u201909)","author":"F Chen","year":"2009","unstructured":"Chen F, Jin D, Meredith P, Ro\u015fu G (2009) Monitoring oriented programming\u2014a project overview. In: Proceedings of the fourth international conference on intelligent computing and information systems (ICICIS\u201909). ACM, New York, pp 72\u201377"},{"key":"139_CR12","volume-title":"Engineering a compiler","author":"KD Cooper","year":"2004","unstructured":"Cooper KD, Torczon L (2004) Engineering a compiler. Morgan Kaufmann, San Mateo"},{"key":"139_CR13","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C Courcoubetis","year":"1992","unstructured":"Courcoubetis C, Vardi M, Wolper P, Yannakakis M (1992) Memory efficient algorithms for the verification of temporal properties. Form Methods Syst Des 1:275\u2013288","journal-title":"Form Methods Syst Des"},{"key":"139_CR14","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/11513988_36","volume-title":"Proc 17th international conference on computer aided verification","author":"M d\u2019Amorim","year":"2005","unstructured":"d\u2019Amorim M, Rosu G (2005) Efficient monitoring of \u03c9-languages. In: Proc 17th international conference on computer aided verification, pp 364\u2013378"},{"key":"139_CR15","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"CAV\u201999: Proc 11th int conf on computer aided verification","author":"M Daniele","year":"1999","unstructured":"Daniele M, Giunchiglia F, Vardi MY (1999) Improved automata generation for linear temporal logic. In: CAV\u201999: Proc 11th int conf on computer aided verification. Springer, London, pp 249\u2013260"},{"key":"139_CR16","author":"A Duret-Lutz","year":"2004","unstructured":"Duret-Lutz A, Poitrenaud D (2004) SPOT: An extensible model checking library using transition-based generalized B\u00fcchi automata. Modeling Anal Simul Comput Syst. doi: 10.1109\/MASCOT.2004.1348184","journal-title":"Modeling Anal Simul Comput Syst"},{"key":"139_CR17","volume-title":"A practical introduction to PSL","author":"C Eisner","year":"2006","unstructured":"Eisner C, Fisman D (2006) A practical introduction to PSL. Springer, New York"},{"issue":"2","key":"139_CR18","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1023\/B:FORM.0000017718.28096.48","volume":"24","author":"B Finkbeiner","year":"2004","unstructured":"Finkbeiner B, Sipma H (2004) Checking finite traces using alternating automata. Form Methods Syst Des 24(2):101\u2013127. doi: 10.1023\/B:FORM.0000017718.28096.48","journal-title":"Form Methods Syst Des"},{"key":"139_CR19","doi-asserted-by":"crossref","unstructured":"Geilen M (2001) On the construction of monitors for temporal logic properties. Electr Notes Theor Comput Sci 55(2)","DOI":"10.1016\/S1571-0661(04)00252-X"},{"key":"139_CR20","doi-asserted-by":"crossref","first-page":"574","DOI":"10.1145\/309847.310001","volume-title":"DAC\u201999: Proc 36th design automation conference","author":"D Geist","year":"1999","unstructured":"Geist D, Biran G, Arons T, Slavkin M, Nustov Y, Farkas M, Holtz K, Long A, King D, Barret S (1999) A methodology for the verification of a \u201csystem on chip\u201d. In: DAC\u201999: Proc 36th design automation conference. ACM, New York, pp 574\u2013579. doi: 10.1145\/309847.310001"},{"key":"139_CR21","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/11691617_4","volume-title":"Model checking software, 13th int SPIN workshop","author":"J Geldenhuys","year":"2006","unstructured":"Geldenhuys J, Hansen H (2006) Larger automata and less work for LTL model checking. In: Model checking software, 13th int SPIN workshop. LNCS, vol\u00a03925. Springer, Berlin, pp 53\u201370"},{"key":"139_CR22","first-page":"3","volume-title":"Protocol specification, testing, and verification","author":"R Gerth","year":"1995","unstructured":"Gerth R, Peled D, Vardi M, Wolper P (1995) Simple on-the-fly automatic verification of Linear Temporal Logic. In: Dembiski P, Sredniawa M (eds) Protocol specification, testing, and verification. Chapman & Hall, London, pp 3\u201318"},{"key":"139_CR23","first-page":"412","volume-title":"Int conf on automated software engineering","author":"D Giannakopoulou","year":"2001","unstructured":"Giannakopoulou D, Havelund K (2001) Automata-based verification of temporal properties on running programs. In: Int conf on automated software engineering. IEEE, Washington, p 412"},{"key":"139_CR24","volume-title":"System design with SystemC","author":"T Grotker","year":"2002","unstructured":"Grotker T, Liao S, Martin G, Swan S (2002) System design with SystemC. Kluwer Academic, Norwell"},{"key":"139_CR25","volume-title":"Standard for property specification language (PSL). IEC 62531:2007 (E)","author":"IEEE working group","year":"2007","unstructured":"IEEE working group (2007) Standard for property specification language (PSL). IEC 62531:2007 (E), pp 1\u2013156. doi: 10.1109\/IEEESTD.2007.4408637"},{"key":"139_CR26","first-page":"131","volume":"19","author":"A Gupta","year":"2002","unstructured":"Gupta A (2002) Assertion-based verification turns the corner. IEEE Des Test Comput 19:131\u2013132. doi: 10.1109\/MDT.2002.10025","journal-title":"IEEE Des Test Comput"},{"key":"139_CR27","unstructured":"Hoos HH (2008) Computer-aided design of high-performance algorithms. Tech rep, University of British Columbia"},{"key":"139_CR28","volume-title":"Introduction to automata theory, languages, and computation","author":"J Hopcroft","year":"1979","unstructured":"Hopcroft J, Ullman J (1979) Introduction to automata theory, languages, and computation. Addison-Wesley, Reading"},{"key":"139_CR29","series-title":"LNCS","first-page":"189","volume-title":"Automatic verification methods for finite state systems, Proc international workshop","author":"C Jard","year":"1989","unstructured":"Jard C, Jeron T (1989) On-line model-checking for finite linear temporal logic specifications. In: Automatic verification methods for finite state systems, Proc international workshop, Grenoble. LNCS, vol 407. Springer, Grenoble, pp 189\u2013196"},{"key":"139_CR30","first-page":"415","volume-title":"Programming language design and implementation (PLDI\u201911)","author":"D Jin","year":"2011","unstructured":"Jin D, Meredith P, Griffith D, Ro\u015fu G (2011) Garbage collection for monitoring parametric properties. In: Programming language design and implementation (PLDI\u201911). ACM, New York, pp 415\u2013424. doi: 10.1145\/1993316.1993547"},{"key":"139_CR31","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/11901914_11","volume-title":"ATVA\u201906: Proc of the international symposium on automated technology for verification and analysis","author":"O Kupferman","year":"2006","unstructured":"Kupferman O, Lampert R (2006) On the construction of fine automata for safety properties. In: ATVA\u201906: Proc of the international symposium on automated technology for verification and analysis, pp 110\u2013124"},{"issue":"3","key":"139_CR32","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman O, Vardi M (2001) Model checking of safety properties. Form Methods Syst Des 19(3):291\u2013314","journal-title":"Form Methods Syst Des"},{"key":"139_CR33","author":"P Meredith","year":"2011","unstructured":"Meredith P, Jin D, Griffith D, Chen F, Ro\u015fu G (2011) An overview of the MOP runtime verification framework. Int J Softw Tech Technol Transfer. doi: 10.1007\/s10009-011-0198-6","journal-title":"Int J Softw Tech Technol Transfer"},{"key":"139_CR34","unstructured":"M\u00f8ller A (2004) http:\/\/www.brics.dk\/automaton\/"},{"key":"139_CR35","first-page":"1246","volume-title":"DATE\u201906: Proc conf on design, automation and test in Europe","author":"K Morin-Allory","year":"2006","unstructured":"Morin-Allory K, Borrione D (2006) Proven correct monitors from PSL specifications. In: DATE\u201906: Proc conf on design, automation and test in Europe, European Design and Automation Association, pp 1246\u20131251"},{"key":"139_CR36","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"TACAS\u201908: Tools and algorithms for the construction and analysis of systems, 14th international conference","author":"LM Moura de","year":"2008","unstructured":"de Moura LM, Bj\u00f8rner N (2008) Z3: An efficient SMT solver. In: TACAS\u201908: Tools and algorithms for the construction and analysis of systems, 14th international conference, pp 337\u2013340"},{"key":"139_CR37","doi-asserted-by":"crossref","first-page":"1346","DOI":"10.1109\/TC.2008.74","volume":"57","author":"L Pierre","year":"2008","unstructured":"Pierre L, Ferro L (2008) A tractable and fast method for monitoring SystemC TLM specifications. IEEE Trans Comput 57:1346\u20131356. doi: 10.1109\/TC.2008.74","journal-title":"IEEE Trans Comput"},{"key":"139_CR38","unstructured":"R\u00f6nkk\u00f6 M (2011) LBT: LTL to B\u00fcchi conversion. Available online (1999). http:\/\/www.tcs.hut.fi\/Software\/maria\/tools\/lbt\/ . Accessed March 29, 2011"},{"key":"139_CR39","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Proc 14th int SPIN conference on model checking software","author":"KY Rozier","year":"2007","unstructured":"Rozier KY, Vardi MY (2007) LTL satisfiability checking. In: Proc 14th int SPIN conference on model checking software. Springer, Berlin, pp 149\u2013167"},{"issue":"4","key":"139_CR40","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/j.entcs.2006.02.007","volume":"144","author":"V Stolz","year":"2006","unstructured":"Stolz V, Bodden E (2006) Temporal assertions using AspectJ. Electron Notes Theor Comput Sci 144(4):109\u2013124. doi: 10.1016\/j.entcs.2006.02.007","journal-title":"Electron Notes Theor Comput Sci"},{"key":"139_CR41","first-page":"123","volume-title":"Proc 8th int\u2019l conf on formal methods and models for codesign","author":"D Tabakov","year":"2010","unstructured":"Tabakov D, Vardi M (2010) Monitoring temporal SystemC properties. In: Proc 8th int\u2019l conf on formal methods and models for codesign. IEEE, New York, pp 123\u2013132"},{"key":"139_CR42","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/FMCAD.2008.ECP.26","volume-title":"FMCAD\u201908: Proc int conf on formal methods in computer-aided design","author":"D Tabakov","year":"2008","unstructured":"Tabakov D, Vardi M, Kamhi G, Singerman E (2008) A temporal language for SystemC. In: FMCAD\u201908: Proc int conf on formal methods in computer-aided design. IEEE Press, New York, pp 1\u20139. http:\/\/portal.acm.org\/citation.cfm?id=1517446"},{"key":"139_CR43","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/11591191_28","volume-title":"LPAR\u201905: 12th int conf on logic for programming, artificial intelligence, and reasoning","author":"D Tabakov","year":"2005","unstructured":"Tabakov D, Vardi MY (2005) Experimental evaluation of classical automata constructions. In: LPAR\u201905: 12th int conf on logic for programming, artificial intelligence, and reasoning, pp 396\u2013411"},{"issue":"1","key":"139_CR44","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M Vardi","year":"1994","unstructured":"Vardi M, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1\u201337","journal-title":"Inf Comput"},{"key":"139_CR45","volume-title":"A practical guide for SystemVerilog assertions","author":"S Vijayaraghavan","year":"2005","unstructured":"Vijayaraghavan S, Ramanathan M (2005) A practical guide for SystemVerilog assertions. Springer, New York"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0139-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0139-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0139-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,13]],"date-time":"2023-06-13T19:08:54Z","timestamp":1686683334000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0139-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,19]]},"references-count":45,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,12]]}},"alternative-id":["139"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0139-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,1,19]]}}}