{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:02Z","timestamp":1760202602943},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2009,10,2]],"date-time":"2009-10-02T00:00:00Z","timestamp":1254441600000},"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":[[2010,6]]},"DOI":"10.1007\/s10703-009-0085-x","type":"journal-article","created":{"date-parts":[[2009,10,1]],"date-time":"2009-10-01T18:36:36Z","timestamp":1254422196000},"page":"114-130","source":"Crossref","is-referenced-by-count":16,"title":["Analog property checkers: a DDR2 case study"],"prefix":"10.1007","volume":"36","author":[{"given":"Kevin D.","family":"Jones","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor","family":"Konrad","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dejan","family":"Ni\u010dkovi\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,10,2]]},"reference":[{"key":"85_CR1","series-title":"LNCS","first-page":"538","volume-title":"Proc CAV\u201900","author":"Y Abarbanel","year":"2000","unstructured":"Abarbanel Y, Beer I, Glushovsky L, Keidar S, Wolfsthal Y (2000) FoCs: automatic generation of simulation checkers from formal specifications. In: Proc CAV\u201900. LNCS, vol 1855. Springer, Berlin, pp 538\u2013542"},{"key":"85_CR2","unstructured":"Accelera Standard. SystemVerilog 3.1a Language reference manual"},{"key":"85_CR3","doi-asserted-by":"crossref","unstructured":"Asarin E, Dang T, Frehse G, Girard A, Le Guernic C, Maler O (2006) Recent progress in continuous and hybrid reachability analysis. In: CACSD","DOI":"10.1109\/CACSD-CCA-ISIC.2006.4776877"},{"key":"85_CR4","doi-asserted-by":"crossref","unstructured":"Alur R, Etessami K, La Torre S, Peled D (1999) Parametric temporal logic for \u201cmodel measuring\u201d. In: ICALP\u201999, pp 159\u2013168","DOI":"10.1007\/3-540-48523-6_13"},{"key":"85_CR5","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur R, Feder T, Henzinger TA (1996) The benefits of relaxing punctuality. J Assoc Comput Mach 43:116\u2013146","journal-title":"J Assoc Comput Mach"},{"key":"85_CR6","unstructured":"Al Sammane G, Zaki MH, Dong ZJ, Tahar S (2007) Towards assertion based verification of analog and mixed signal designs using PSL. In: FDL\u201907"},{"key":"85_CR7","unstructured":"Dastidar TR, Chakrabarti PP (2005) Verification system for transient response of analog circuits using model checking. In: VLSID\u201905, pp 195\u2013200"},{"key":"85_CR8","series-title":"LNCS","first-page":"323","volume-title":"Proc SPIN\u201900","author":"D Drusinsky","year":"2000","unstructured":"Drusinsky D (2000) The temporal rover and the ATG rover. In: Proc SPIN\u201900. LNCS, vol 1885. Springer, Berlin, pp 323\u2013330"},{"key":"85_CR9","series-title":"LNCS","first-page":"171","volume-title":"Proc FORMATS\u201906","author":"G Fainekos","year":"2006","unstructured":"Fainekos G, Girard A, Pappas G (2006) Temporal logic verification using simulation. In: Proc FORMATS\u201906. LNCS, vol 4202. Springer, Berlin, pp 171\u2013186"},{"key":"85_CR10","unstructured":"Gerth R, Peled DA, Vardi MY, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In: PSTV, pp 3\u201318"},{"key":"85_CR11","series-title":"LNCS","first-page":"53","volume-title":"CAV\u201901","author":"P Gastin","year":"2001","unstructured":"Gastin P, Oddoux D (2001) Fast LTL to B\u00fcchi automata translation. In: CAV\u201901. LNCS, vol 2101. Springer, Berlin, pp 53\u201365"},{"key":"85_CR12","unstructured":"Havlicek J, Fisman D, Eisner C (2004) Basic results on the semantics of Accelera PSL 1.1 foundation language. In: Technical report 2004.02, Accelera"},{"key":"85_CR13","unstructured":"Hartong W, Hedrich L, Barke E (2002) Model checking algorithms for analog verification. In: DAC\u201902"},{"key":"85_CR14","unstructured":"Havelund K, Rosu G (2001) Java PathExplorer\u2014a runtime verification tool. In: Proc. ISAIRAS\u201901"},{"key":"85_CR15","unstructured":"JEDEC Standard. JESD79-2C DDR2 SRAM specification"},{"key":"85_CR16","unstructured":"Jesser A, L\u00e4mmermann S, Pacholik A, Weiss R, Ruf J, Fengler W, Hedrich L, Kropf T, Rosenstiel\u00a0W (2007) Analog simulation meets digital verification\u2014a formal assertion approach for mixed-signal verification. In: SASIMI\u201907, pp 507\u2013514"},{"key":"85_CR17","doi-asserted-by":"crossref","unstructured":"Kim M, Lee I, Sammapun U, Shin J, Sokolsky O (2002) Monitoring, checking, and steering of real-time systems. In: Proc. RV\u201902. ENTCS 70(4)","DOI":"10.1016\/S1571-0661(04)80579-6"},{"key":"85_CR18","doi-asserted-by":"crossref","unstructured":"Little S, Seegmiller N, Walter D, Myers CJ, Yoneda T (2006) Verification of analog\/mixed-signal circuits using labeled hybrid petri-nets. In: ICCAD\u201906, pp 275\u2013282","DOI":"10.1145\/1233501.1233556"},{"key":"85_CR19","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/BFb0032003","volume-title":"Real-time: theory in practice","author":"O Maler","year":"1992","unstructured":"Maler O, Manna Z, Pnueli A (1992) From timed to hybrid systems. In: Real-time: theory in practice. LNCS, vol 600. Springer, Berlin, pp 447\u2013484"},{"key":"85_CR20","doi-asserted-by":"crossref","unstructured":"Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signal. In: FORMATS\/FTRTFT\u201904, pp 152\u2013166","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"85_CR21","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 (1995) Temporal verification of reactive systems: safety. Springer, Berlin"},{"key":"85_CR22","unstructured":"Nickovic D (2008) Checking timed and hybrid properties: theory and practice. PhD thesis"},{"key":"85_CR23","doi-asserted-by":"crossref","unstructured":"Nahhal T, Dang T (2007) Test coverage for continuous and hybrid systems. In: CAV\u201907, pp 449\u2013462","DOI":"10.1007\/978-3-540-73368-3_47"},{"key":"85_CR24","doi-asserted-by":"crossref","unstructured":"Nahhal T, Dang T (2007) Guided randomized simulation. In: HSCC\u201907, pp 731\u2013735","DOI":"10.1007\/978-3-540-71493-4_72"},{"key":"85_CR25","doi-asserted-by":"crossref","unstructured":"Nickovic D, Maler O (2007) AMT: a property-based monitoring tool for analog systems. In: FORMATS\u201907, pp 304\u2013319","DOI":"10.1007\/978-3-540-75454-1_22"},{"key":"85_CR26","series-title":"LNCS","first-page":"248","volume-title":"CAV\u201900","author":"F Somenzi","year":"2000","unstructured":"Somenzi F, Bloem R (2000) Efficient B\u00fcchi automata from LTL formulae. In: CAV\u201900. LNCS, vol 1855. Springer, Berlin, pp 248\u2013263"},{"key":"85_CR27","unstructured":"Steinhorst S, Hedrich L (2008) Model checking of analog systems using an analog specification language. In: DATE\u201908, pp 324\u2013329"},{"key":"85_CR28","unstructured":"Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: LICS\u201986, pp 322\u2013331"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0085-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-009-0085-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0085-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:51Z","timestamp":1559253951000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-009-0085-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,10,2]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,6]]}},"alternative-id":["85"],"URL":"https:\/\/doi.org\/10.1007\/s10703-009-0085-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,10,2]]}}}