{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T07:09:30Z","timestamp":1726124970610},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319238197"},{"type":"electronic","value":"9783319238203"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23820-3_6","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T14:21:39Z","timestamp":1442672499000},"page":"87-101","source":"Crossref","is-referenced-by-count":14,"title":["Assuring the Guardians"],"prefix":"10.1007","author":[{"given":"Jonathan","family":"Laurent","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alwyn","family":"Goodloe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lee","family":"Pike","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,15]]},"reference":[{"issue":"3","key":"6_CR1","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Automat. Reasoning 44(3), 175\u2013205 (2010)","journal-title":"J. Automat. Reasoning"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Caspi, P., Pialiud, D., Halbwachs, N., Plaice, J.: LUSTRE: a declarative language for programming synchronous systems. In: 14th Symposium on Principles of Programming Languages, pp. 178\u2013188 (1987)","DOI":"10.1145\/41625.41641"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Bounded model checking and induction: from refutation to verification. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 14\u201326. Springer, Heidelberg (2003)","DOI":"10.1007\/978-3-540-45069-6_2"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Heidelberg (2014)"},{"issue":"4","key":"6_CR5","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4), 543\u2013560 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Torlak, E., Bodik, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 530\u2013541. ACM (2014)","DOI":"10.1145\/2666356.2594340"},{"issue":"6","key":"6_CR7","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/2605205","volume":"57","author":"A Gill","year":"2014","unstructured":"Gill, A.: Domain-specific languages and code synthesis using Haskell. Commun. ACM 57(6), 42\u201349 (2014)","journal-title":"Commun. ACM"},{"key":"6_CR8","unstructured":"Hagen, G.: Verifying safety properties of Lustre programs: an SMT-based approach. PhD thesis, University of Iowa (2008)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Hagen, G., Tinelli, C.: Scaling up the formal verification of lustre programs with SMT-based techniques. In: Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2008). IEEE (2008)","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"key":"6_CR10","series-title":"Workshops in Computing","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-1-4471-3227-1_8","volume-title":"Algebraic Methodology and Software Technology","author":"N Halbwachs","year":"1994","unstructured":"Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) AMAST 1993. Workshops in Computing, pp. 83\u201396. Springer, London (1994)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-540-68524-1_3","volume-title":"Testing of Software and Communicating Systems","author":"K Havelund","year":"2008","unstructured":"Havelund, K.: Runtime verification of C programs. In: Suzuki, K., Higashino, T., Ulrich, A., Hasegawa, T. (eds.) TestCom\/FATES 2008. LNCS, vol. 5047, pp. 7\u201322. Springer, Heidelberg (2008)"},{"issue":"2","key":"6_CR12","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/s10009-003-0117-6","volume":"6","author":"K Havelund","year":"2004","unstructured":"Havelund, K., Ro\u015fu, G.: Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Transf. 6(2), 158\u2013173 (2004)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"6_CR13","unstructured":"Hesselink, W.H.: The Boyer-Moore majority vote algorithm (2005)"},{"key":"6_CR14","unstructured":"Jones, S.P. (ed.): Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge (2002). \n                      http:\/\/haskell.org\/"},{"key":"6_CR15","unstructured":"Mik\u00e1\u0107, J., Caspi, P.: Formal system development with Lustre: Framework and example. Technical Report TR-2005-11, Verimag Technical Report (2005)"},{"key":"6_CR16","unstructured":"Moore, S.J., Boyer, R.S.: MJRTY - A Fast Majority Vote Algorithm. Technical Report 1981\u201332, Institute for Computing Science, University of Texas, February 1981"},{"key":"6_CR17","unstructured":"University of Iowa: Kind Research Group. Kind 2: Multi-engine SMT-based Automatic Model Checker. \n                      http:\/\/kind2-mc.github.io\/kind2\/"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-16612-9_26","volume-title":"Runtime Verification","author":"L Pike","year":"2010","unstructured":"Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: a hard real-time runtime monitor. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 345\u2013359. Springer, Heidelberg (2010)"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Pike, L., Hickey, P.C., Bielman, J., Elliott, T., DuBuisson, T., Launchbury, J.: Programming languages for high-assurance autonomous vehicles: extended abstract. In: Programming Languages Meets Program Verification, pp. 1\u20132. ACM (2014)","DOI":"10.1145\/2541568.2541570"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-29860-8_23","volume-title":"Runtime Verification","author":"L Pike","year":"2012","unstructured":"Pike, L., Niller, S., Wegmann, N.: Runtime verification for ultra-critical systems. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 310\u2013324. Springer, Heidelberg (2012)"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Pike, L., Wegmann, N., Niller, S., Goodloe, A.: Experience report: a do-it-yourself high-assurance compiler. In: Proceedings of the International Conference on Functional Programming (ICFP). ACM, September 2012","DOI":"10.1145\/2364527.2364553"},{"issue":"4","key":"6_CR22","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s11334-013-0223-x","volume":"9","author":"L Pike","year":"2013","unstructured":"Pike, L., Wegmann, N., Niller, S., Goodloe, A.: Copilot: monitoring embedded systems. Innovations Syst. Softw. Eng. 9(4), 235\u2013255 (2013)","journal-title":"Innovations Syst. Softw. Eng."},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Uhler, R., Dave, N.: Smten with satisfiability-based search. In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2014, pp. 157\u2013176. ACM (2014)","DOI":"10.1145\/2714064.2660208"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-89247-2_2","volume-title":"Runtime Verification","author":"J Rushby","year":"2008","unstructured":"Rushby, J.: Runtime certification. In: Leucker, M. (ed.) RV 2008. LNCS, vol. 5289, pp. 21\u201335. Springer, Heidelberg (2008)"},{"key":"6_CR25","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"6_CR26","unstructured":"Somenzi, F., Bradley, A.R.: Ic3: where monolithic and incremental meet. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, FMCAD 2011, pp. 3\u20138. FMCAD Inc. (2011)"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23820-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T00:41:00Z","timestamp":1559263260000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-23820-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319238197","9783319238203"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23820-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}