{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:58:19Z","timestamp":1725512299107},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540714095"},{"type":"electronic","value":"9783540714101"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71410-1_9","type":"book-chapter","created":{"date-parts":[[2007,5,21]],"date-time":"2007-05-21T06:57:52Z","timestamp":1179730672000},"page":"111-126","source":"Crossref","is-referenced-by-count":1,"title":["On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors"],"prefix":"10.1007","author":[{"given":"Simon","family":"Winwood","sequence":"first","affiliation":[]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[]},{"given":"Manuel M. T.","family":"Chakravarty","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Proc. of POPL\u201997, Paris, Jan.1997, pp. 106\u2013119 (1997), http:\/\/raw.cs.berkeley.edu\/Papers\/pcc_popl97.ps","DOI":"10.1145\/263699.263712"},{"issue":"3","key":"9_CR2","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. TOPLAS\u00a021(3), 527\u2013568 (1999)","journal-title":"TOPLAS"},{"key":"9_CR3","first-page":"333","volume-title":"Proc. of PLDI\u201998, vol. 33,5","author":"G.C. Necula","year":"1998","unstructured":"Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. In: Proc. of PLDI\u201998, vol. 33,5, Jun. 17\u201319, pp. 333\u2013344. ACM Press, New York (1998), http:\/\/www.cs.cmu.edu\/~necula\/pldi98.ps.gz"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D. Aspinall","year":"2005","unstructured":"Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D., Stark, I.: Mobile resource guarantees for smart devices. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 1\u201326. Springer, Heidelberg (2005)"},{"key":"9_CR5","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)"},{"issue":"1","key":"9_CR6","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F.B. Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. Information and System Security\u00a03(1), 30\u201350 (2000)","journal-title":"Information and System Security"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/11679219_13","volume-title":"Formal Aspects in Security and Trust","author":"S. Winwood","year":"2006","unstructured":"Winwood, S., Chakravarty, M.M.T.: Secure untrusted binaries - provably! In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol.\u00a03866, pp. 171\u2013186. Springer, Heidelberg (2006)"},{"key":"9_CR8","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1109\/SECPRI.1989.36295","volume-title":"IEEE Symposium on Security and Privacy","author":"D.F.C. Brewer","year":"1989","unstructured":"Brewer, D.F.C., Nash, M.J.: The Chinese Wall security policy. In: IEEE Symposium on Security and Privacy, pp. 206\u2013214. IEEE Computer Society Press, Los Alamitos (1989)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Havelund","year":"2002","unstructured":"Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, pp. 342\u2013356. Springer, Heidelberg (2002)"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/11679219_9","volume-title":"Formal Aspects in Security and Trust","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Rezk, T., Saabas, A.: Proof obligations preserving compilation. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol.\u00a03866, pp. 112\u2013126. Springer, Heidelberg (2006)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/BFb0013024","volume-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","author":"Z. Manna","year":"1989","unstructured":"Manna, Z., Pnueli, A.: The anchored version of the temporal framework. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol.\u00a0354, pp. 201\u2013284. Springer, Heidelberg (1989)"},{"key":"9_CR12","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/978-94-010-0413-8_11","volume-title":"Proof and System-Reliability","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics in Isabelle\/HOL. In: Schwichtenberg, H., Steinbr\u00fcggen, R. (eds.) Proof and System-Reliability, pp. 341\u2013367. Kluwer Academic Publishers, Dordrecht (2002)"},{"issue":"1","key":"9_CR13","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1093\/jigpal\/8.1.55","volume":"8","author":"O. Lichtenstein","year":"2000","unstructured":"Lichtenstein, O., Pnueli, A.: Propositional temporal logics: Decidability and completeness. Logic Journal of the IGPL\u00a08(1), 55\u201385 (2000), http:\/\/www.wisdom.weizmann.ac.il\/~amir\/lp00.ps.gz","journal-title":"Logic Journal of the IGPL"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Geilen, M.: On the construction of monitors for temporal logic properties. In: Electr. Notes Theor. Comput. Sci., vol. 55 (2001), http:\/\/www.ics.ele.tue.nl\/~mgeilen\/publications\/rv2001.pdf","DOI":"10.1016\/S1571-0661(04)00252-X"},{"key":"9_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-45620-1_3","volume-title":"Automated Deduction - CADE-18","author":"A. Bernard","year":"2002","unstructured":"Bernard, A., Lee, P.: Temporal logic for proof-carrying code. In: Voronkov, A. (ed.) Automated Deduction - CADE-18. LNCS (LNAI), vol.\u00a02392, pp. 31\u201346. Springer, Heidelberg (2002)"},{"issue":"5","key":"9_CR16","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Trans. Software Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","first-page":"357","volume-title":"Formal Methods and Software Engineering","author":"F. Chen","year":"2004","unstructured":"Chen, F., D\u2019Amorim, M., Rosu, G.: A formal monitoring-based framework for software development and analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 357\u2013372. Springer, Heidelberg (2004)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/11513988_36","volume-title":"Computer Aided Verification","author":"M. D\u2019Amorim","year":"2005","unstructured":"D\u2019Amorim, M., Rosu, G.: Efficient monitoring of omega-languages. . In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 364\u2013378. Springer, Heidelberg (2005)"},{"key":"9_CR19","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Program monitoring with LTL in EAGLE. In: Proc. of PADTAD\u201904, April (2004), http:\/\/www.havelund.com\/Publications\/eagle-padtad04.pdf"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45139-0_1","volume-title":"Model Checking Software","author":"D. Peled","year":"2001","unstructured":"Peled, D., Zuck, L.: From model checking to a temporal proof. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol.\u00a02057, pp. 1\u201314. Springer, Heidelberg (2001)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002), http:\/\/www4.in.tum.de\/~nipkow\/LNCS2283\/tutorial.pdf"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71410-1_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:19:47Z","timestamp":1605745187000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71410-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540714095","9783540714101"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71410-1_9","relation":{},"subject":[]}}