{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:40Z","timestamp":1725516520188},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_33","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"308-317","source":"Crossref","is-referenced-by-count":0,"title":["Can We Build an Automatic Program Verifier? Invariant Proofs and Other Challenges"],"prefix":"10.1007","author":[{"given":"Myla","family":"Archer","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"1-4","key":"33_CR1","first-page":"139","volume":"29","author":"M. Archer","year":"2001","unstructured":"Archer, M.: TAME: Using PVS strategies for special-purpose theorem proving. Annals of Mathematics and Artificial Intelligence\u00a029(1-4), 139\u2013181 (2001)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Archer, M.: Proving correctness of the basic TESLA multicast stream authentication protocol with TAME. In: Workshop on Issues in the Theory of Security (WITS 2002), Portland, OR, January 14\u201315 (2002)","DOI":"10.21236\/ADA464932"},{"issue":"3","key":"33_CR3","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1023\/A:1016320523091","volume":"9","author":"M. Archer","year":"2002","unstructured":"Archer, M., Heitmeyer, C., Riccobene, E.: Proving invariants of I\/O automata with TAME. Automated Software Engineering\u00a09(3), 201\u2013232 (2002)","journal-title":"Automated Software Engineering"},{"issue":"1","key":"33_CR4","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N. Bj\u00f8rner","year":"1997","unstructured":"Bj\u00f8rner, N., Browne, I.A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theoretical Computer Science\u00a0173(1), 49\u201387 (1997)","journal-title":"Theoretical Computer Science"},{"key":"33_CR5","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence\u00a062, 185\u2013253 (1993)","journal-title":"Artificial Intelligence"},{"key":"33_CR6","series-title":"Automated Reasoning Series","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-94-011-3488-0_7","volume-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","author":"A. Bundy","year":"1991","unstructured":"Bundy, A.: The use of proof plans for normalization. In: Boyer, R.S. (ed.) Automated Reasoning: Essays in Honor of Woody Bledsoe. Automated Reasoning Series, vol.\u00a07, pp. 149\u2013166. Kluwer, Dordrecht (1991)"},{"issue":"10","key":"33_CR7","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013583 (1969)","journal-title":"Communications of the ACM"},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 1977 Symp. on Principles of Programming Languages (January, 1977)","DOI":"10.1145\/512950.512973"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables. In: Proc. 1978 Symp. on Principles of Programming Languages (January, 1978)","DOI":"10.1145\/512760.512770"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Ernst, M.: Dynamically Discovering Likely Program Invariants. PhD thesis, Univ. of Washington (2000)","DOI":"10.1145\/302405.302467"},{"key":"33_CR12","series-title":"Mathematical Aspects of Computer Science","first-page":"19","volume-title":"Proceedings of Symposia in Applied Mathematics","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proceedings of Symposia in Applied Mathematics. Mathematical Aspects of Computer Science, vol.\u00a019, pp. 19\u201332. American Mathematical Society, Providence, RI (1967)"},{"key":"33_CR13","unstructured":"Garland, S.: TIOA User Guide and Reference Manual. Technical report, MIT CSAIL, Cambridge, MA, URL (2006), http:\/\/tioa.csail.mit.edu"},{"issue":"1","key":"33_CR14","first-page":"19","volume":"20","author":"C. Heitmeyer","year":"2005","unstructured":"Heitmeyer, C., Archer, M., Bharadwaj, R., Jeffords, R.: Tools for constructing requirements specifications: The SCR toolset at the age of ten. International Journal on Computer System Science and Engineering\u00a020(1), 19\u201335 (2005)","journal-title":"International Journal on Computer System Science and Engineering"},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"Jeffords, R., Heitmeyer, C.: Automatic generation of state invariants from requirements specifications. In: Proc. 6th International Symposium on the Foundations of Software Engineering (FSE-6), Orlando, FL (November 1998)","DOI":"10.1145\/288195.288218"},{"key":"33_CR16","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)"},{"volume-title":"Computer-Aided Reasoning: Case Studies","year":"2000","key":"33_CR17","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: Case Studies. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"33_CR18","unstructured":"Kaynar, D., Lynch, N.A., Segala, R., Vaandrager, F.: A mathematical framework for modeling and analyzing real-time systems. In: The 24th IEEE Intern. Real-Time Systems Symposium (RTSS), Cancun, Mexico (December 2003)"},{"issue":"3","key":"33_CR19","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1023\/A:1006059810729","volume":"21","author":"M. Kerber","year":"1998","unstructured":"Kerber, M., Kohlhase, M., Sorge, V.: Integrating computer algebra into proof planning. Journal of Automated Reasoning\u00a021(3), 327\u2013355 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR20","volume-title":"Proc. 15th Annual Computer Security Applications Conference (ACSAC 1999)","author":"J. Kirby Jr.","year":"1999","unstructured":"Kirby Jr., J., Archer, M., Heitmeyer, C.: SCR: A practical approach to building a high assurance COMSEC system. In: Proc. 15th Annual Computer Security Applications Conference (ACSAC 1999), IEEE Comp. Soc. Press, Los Alamitos (1999)"},{"issue":"3","key":"33_CR21","first-page":"219","volume":"2","author":"N. Lynch","year":"1989","unstructured":"Lynch, N., Tuttle, M.: An introduction to Input\/Output automata. CWI-Quarterly\u00a02(3), 219\u2013246 (1989)","journal-title":"CWI-Quarterly"},{"issue":"1","key":"33_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1996.0060","volume":"128","author":"N. Lynch","year":"1996","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations \u2013 Part II: Timing-based systems. Information and Computation\u00a0128(1), 1\u201325 (1996)","journal-title":"Information and Computation"},{"issue":"2","key":"33_CR23","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.entcs.2005.01.005","volume":"125","author":"S. Mitra","year":"2005","unstructured":"Mitra, S., Archer, M.: PVS strategies for proving abstraction properties of automata. Electronic Notes in Theor. Comp. Sci.\u00a0125(2), 45\u201365 (2005)","journal-title":"Electronic Notes in Theor. Comp. Sci."},{"key":"33_CR24","unstructured":"Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Prover Guide, Version 2.4. Technical report, Comp. Sci. Lab. SRI Intl. Menlo Park, CA (November 2001)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T03:43:05Z","timestamp":1557718985000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}