{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T16:33:04Z","timestamp":1725726784690},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540108597"},{"type":"electronic","value":"9783662023280"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1981]]},"DOI":"10.1007\/978-3-662-02328-0_24","type":"book-chapter","created":{"date-parts":[[2013,5,23]],"date-time":"2013-05-23T14:23:38Z","timestamp":1369319018000},"page":"256-276","source":"Crossref","is-referenced-by-count":0,"title":["Program Veriflcation at Stanford: Past, Present, Future"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"Polak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Research report RC 7859","volume-title":"A program development tool","author":"CN Alberga","year":"1979","unstructured":"Alberga, C. N., et. al.: A program development tool, Research report RC 7859, IBM 1979."},{"key":"24_CR2","volume-title":"Stanford Resolution Theorem Prover: A user manual","author":"JR Allen","year":"1971","unstructured":"Allen J. R. : Stanford Resolution Theorem Prover: A user manual, Stanford Artificial Intelligence Lab. Operating Note, 1971.."},{"key":"24_CR3","volume-title":"Putting theories together to make specifications, hit","author":"RM Burstall","year":"1977","unstructured":"Burstall, R. M., Goguen, J. A.: Putting theories together to make specifications, hit. Joint Conf. on Artifical Intelligence, Boston 1977."},{"key":"24_CR4","unstructured":"Cartright, R., Oppen, D.: The Logic of Aliasing, STAN-CS-79\u2013740."},{"key":"24_CR5","series-title":"Report CSL-73-1","volume-title":"An interactive program verifier","author":"LP Deutsch","year":"1973","unstructured":"Deutsch, L. P.: An interactive program verifier, Report CSL-73\u20131, XEROX PARC, 1973."},{"key":"24_CR6","volume-title":"Applied Mathematics 19","author":"R Floyd","year":"1967","unstructured":"Floyd, R. W.: Assigning Meanings to Programs, Proceedings of Symp. in Applied Mathematics 19 (1967)."},{"key":"24_CR7","first-page":"105","volume-title":"Proc. 5th. ACM Symp. on Principles of Programming Languages, Tucson","author":"SM German","year":"1978","unstructured":"German, S.M.: Automating proofs of the absence of common runtime errors, Proc. 5th. ACM Symp. on Principles of Programming Languages, Tucson, 1978, pp 105\u2013118."},{"key":"24_CR8","unstructured":"German, S.M.: An extended semantic definition of Pascal for proving the absence of common runtime errors, STAN-CS-80\u2013811."},{"key":"24_CR9","unstructured":"Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF, Report CSR-11\u201377, University of Edinburgh."},{"key":"24_CR10","volume-title":"Automatic Program Verification III: A Methodology for Verifying Programs","author":"FW Henke von","year":"1974","unstructured":"von Henke F. W., Luckham D. C.: Automatic Program Verification III: A Methodology for Verifying Programs, AIM-256, 1974."},{"key":"24_CR11","first-page":"576","volume-title":"An Axiomatic Basis of Computer Programming","author":"CA Hoare","year":"1969","unstructured":"Hoare, C. A. R.: An Axiomatic Basis of Computer Programming, CACM 12, Oct, pp 576\u2013580 (1969)."},{"key":"24_CR12","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/BF00289504","volume":"2","author":"CAR Hoare","year":"1973","unstructured":"Hoare, C. A. R., Wirth, N.: An Axiomatic Definition of the Programming language Pascal, Acta Informatica, 2 (1973), pp.335\u2013355.","journal-title":"Acta Informatica"},{"key":"24_CR13","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/BF00288746","volume":"4","author":"S Igarashi","year":"1975","unstructured":"Igarashi, S., London, R. L., Luckham, D. C.: Automatic Program Verification 1: Logical Basis and Its Implementation, Acta Informatica, Vol 4, pp 145\u2013182 (1975).","journal-title":"Acta Informatica"},{"key":"24_CR14","volume-title":"PASCAL, User Manual and Report","author":"K Jensen","year":"1976","unstructured":"Jensen, K., Wirth, N.: PASCAL, User Manual and Report, Springer, New York, Heidelberg, Berlin, 1976."},{"key":"24_CR15","unstructured":"Karp, R. A.: Proving Concurrent Programs Correct, STAN-CS-79\u2013783."},{"key":"24_CR16","volume-title":"Ph. D. Thesis, CMU","author":"JC King","year":"1969","unstructured":"King, J. C.: A program verifier, Ph. D. Thesis, CMU, 1969."},{"key":"24_CR17","volume-title":"Report on the programming language Euclid","author":"BW Lamport","year":"1977","unstructured":"Lamport, B.W., et. al.: Report on the programming language Euclid, Sigplan Notices, Vol. 12, No. 2, 1977."},{"key":"24_CR18","volume-title":"Correctness of two compilers for a LISP subset","author":"R London","year":"1971","unstructured":"London, R. L.: Correctness of two compilers for a LISP subset, AIM - 151, Stanford University, 1971."},{"key":"24_CR19","volume-title":"Proof rules for the programming language Euclid","author":"RL London","year":"1978","unstructured":"London, R.L. et al: Proof rules for the programming language Euclid, Acta Informatica, Vol 10, No 1 (1978)."},{"key":"24_CR20","unstructured":"Luckham, D. C., Polak, W.: ADA Exceptions: Specification and Proof Techniques, STAN\u2014CS-80\u2013789."},{"key":"24_CR21","doi-asserted-by":"crossref","DOI":"10.21236\/ADA019569","volume-title":"Automatic Program Verification IV: Proof of Termination Within a Weak Logic of Programs","author":"DC Luckham","year":"1975","unstructured":"Luckham, D. C., Suzuki, N.: Automatic Program Verification IV: Proof of Termination Within a Weak Logic of Programs, AIM-269, October 1975."},{"key":"24_CR22","doi-asserted-by":"crossref","DOI":"10.21236\/ADA027455","volume-title":"Automatic Program Verification V: Verification-Oriented Proof Rules for Arrays, Records and Pointers","author":"DC Luckham","year":"1976","unstructured":"Luckham, D. C., Suzuki, N.: Automatic Program Verification V: Verification-Oriented Proof Rules for Arrays, Records and Pointers, MM-278, March 1976."},{"key":"24_CR23","volume-title":"Verification of Array, Record, and Pointer Operations in Pascal","author":"DC Luckham","year":"1979","unstructured":"Luckham, D. C., Suzuki, N.: Verification of Array, Record, and Pointer Operations in Pascal, ACM TOPLAS 1\/2, 1979."},{"key":"24_CR24","volume-title":"Correctness of a Compiler for Arithmetic Expressions","author":"J McCarthy","year":"1966","unstructured":"McCarthy, J., Painter, J.: Correctness of a Compiler for Arithmetic Expressions, AIM-40, Stanford University 1966."},{"key":"24_CR25","volume-title":"Proceedings of the ACM Conference on Proving Assertions about Programs, Las Cruces","author":"R Milner","year":"1972","unstructured":"Milner R.: Implementation and applications of Scott\u2019s Logic for Computable Functions., in: Proceedings of the ACM Conference on Proving Assertions about Programs, Las Cruces, 1972."},{"key":"24_CR26","doi-asserted-by":"crossref","DOI":"10.21236\/AD0785072","volume-title":"Logic for Computable Functions: Description of a Machine Implementation","author":"R Milner","year":"1972","unstructured":"Milner, R.: Logic for Computable Functions: Description of a Machine Implementation, AIM-169, May 1972."},{"key":"24_CR27","volume-title":"Hierarchical program specification and verification \u2014 a many-sorted logical approach","author":"R Nakajima","year":"1980","unstructured":"Nakajima, R., Honda, M., Nakahara, L: Hierarchical program specification and verification \u2014 a many-sorted logical approach., Acta Informatica, Vol 14, Fasc. 2, 1980."},{"key":"24_CR28","volume-title":"Simplification by Cooperating Decision Procedures","author":"CG Nelson","year":"1978","unstructured":"Nelson, C. G., Oppen, D. C.: Simplification by Cooperating Decision Procedures, AIM-311, April 1978."},{"key":"24_CR29","volume-title":"Simplification by Cooperating Decision Procedures","author":"CG Nelson","year":"1979","unstructured":"Nelson, C. G., Oppen, D. C.: Simplification by Cooperating Decision Procedures, TOPLAS 2\/1,1979."},{"key":"24_CR30","volume-title":"Fast decision procedures based on congruence closure","author":"CG Nelson","year":"1980","unstructured":"Nelson, C. G., Oppen, D. C.: Fast decision procedures based on congruence closure, JACM 27\/2, 1980."},{"key":"24_CR31","volume-title":"Fast decision procedures based on UNION and FIND","author":"CG Nelson","year":"1977","unstructured":"Nelson, C. G., Oppen, D. C.: Fast decision procedures based on UNION and FIND, Proc 18th Annual Symp. on Foundations of Comp. Science, Providence, RI, 1977."},{"key":"24_CR32","volume-title":"Complexity, convexity, and combinations of theories","author":"D Oppen","year":"1980","unstructured":"Oppen, D. C.: Complexity, convexity, and combinations of theories, TCS 12\/3, 1980."},{"key":"24_CR33","volume-title":"Reasoning about recursively defined data structures","author":"D Oppen","year":"1980","unstructured":"Oppen, D. C.: Reasoning about recursively defined data structures, JACM 27\/2, 1980."},{"key":"24_CR34","volume-title":"An exercise in automatic program verification","author":"W Polak","year":"1979","unstructured":"Polak, W.: An exercise in automatic program verification, IEEE Transactions on Software Engineering, SE-5\/5 (1979)."},{"key":"24_CR35","unstructured":"Polak, W.: Theory of compiler specification and verification, STAN\u2014CS-80\u2013802."},{"key":"24_CR36","volume-title":"Proram verification based on denotational semantics","author":"W Polak","year":"1981","unstructured":"Polak W.: Proram verification based on denotational semantics, Proc. 8th. ACM Symp. on Principles of Programming languages, Williamsburg, 1981."},{"key":"24_CR37","first-page":"290","volume-title":"Reasoning about arrays","author":"JC Reynolds","year":"1979","unstructured":"Reynolds J.C.: Reasoning about arrays, Communications of the ACM 22.5, 1979, 290\u2013299."},{"key":"24_CR38","volume-title":"Stanford Pascal Verifier User Manual","author":"Stanford Verification Group","year":"1979","unstructured":"Stanford Verification Group: Stanford Pascal Verifier User Manual, Stanford Verification Group Report No. 11, 1979."},{"key":"24_CR39","doi-asserted-by":"crossref","unstructured":"Suzuki, N.: Automatic Program Verification II: verifying programs by algebraic and logical reduction, STAN-CS-74\u2013473.","DOI":"10.1145\/390016.808471"},{"key":"24_CR40","first-page":"473","volume-title":"Verifying Programs by Algebraic and Logical Reduction","author":"N Suzuki","year":"1975","unstructured":"Suzuki, N.: Verifying Programs by Algebraic and Logical Reduction, Proceedings of Int\u2019l Conf on Reliable Software, IEEE, pp 473\u2013481 (1975)."},{"key":"24_CR41","volume-title":"Automatic Verification of Programs with Complex Data Structures","author":"N Suzuki","year":"1976","unstructured":"Suzuki, N.: Automatic Verification of Programs with Complex Data Structures, AIM-279, February 1976."},{"key":"24_CR42","unstructured":"Teitelbaum, R. T.: The Cornell Program Synthesizer: A microcomputer Implementation of PL\/CS, Cornell TR 79\u2013370, 1979."}],"container-title":["Informatik-Fachberichte","GWAI-81"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-02328-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,22]],"date-time":"2022-02-22T18:33:43Z","timestamp":1645554823000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-02328-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1981]]},"ISBN":["9783540108597","9783662023280"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-02328-0_24","relation":{},"ISSN":["0343-3005"],"issn-type":[{"type":"print","value":"0343-3005"}],"subject":[],"published":{"date-parts":[[1981]]}}}