{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:55Z","timestamp":1725516535000},"publisher-location":"Berlin, Heidelberg","reference-count":22,"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_55","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"502-509","source":"Crossref","is-referenced-by-count":1,"title":["Programming with Proofs: Language-Based Approaches to Totally Correct Software"],"prefix":"10.1007","author":[{"given":"Aaron","family":"Stump","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"55_CR1","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W. Ahrendt","year":"2005","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.: The KeY tool. Software and System Modeling\u00a04, 32\u201354 (2005)","journal-title":"Software and System Modeling"},{"key":"55_CR2","unstructured":"Altenkirch, T.: Integrated verification in Type Theory. Lecture notes for a course at ESSLLI 96, Prague (1996) (Available from the author\u2019s website)"},{"key":"55_CR3","unstructured":"Brandt, J.: What a Mesh: Dependent Data Types for Correct Mesh Manipulation Algorithms. Master\u2019s thesis, Washington University in Saint Louis, April (2005), http:\/\/cl.cse.wustl.edu"},{"key":"55_CR4","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"55_CR5","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Formal Verification of IA-64 Division Algorithms. In: 13th International Conference on Theorem Proving in Higher Order Logics (2000)","DOI":"10.1007\/3-540-44659-1_15"},{"key":"55_CR6","unstructured":"Klapper, R., Stump, A.: Validated Proof-Producing Decision Procedures. In: Tinelli, C., Ranise, S. (eds.) 2nd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (2004)"},{"issue":"3","key":"55_CR7","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/S0304-3975(02)00869-1","volume":"298","author":"G. Klein","year":"2003","unstructured":"Klein, G., Nipkow, T.: Verified Bytecode Verifiers. Theoretical Computer Science\u00a0298(3), 583\u2013626 (2003)","journal-title":"Theoretical Computer Science"},{"issue":"1-2","key":"55_CR8","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa Tool for Certification of JAVA\/JAVACARD Programs Annotated in JML. Journal of Logic and Algebraic Programming\u00a058(1-2), 89\u2013106 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"55_CR9","doi-asserted-by":"crossref","unstructured":"McBride, C., McKinna, J.: The View from the Left. Journal of Functional Programming\u00a014(1) (2004)","DOI":"10.1017\/S0956796803004829"},{"key":"55_CR10","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11513988_47","volume-title":"17th International Conference on Computer-Aided Verification","author":"S. McPeak","year":"2005","unstructured":"McPeak, S., Necula, G.: Data Structure Specifications via Local Equality Axioms. In: Etessami, K., Rajamani, S. (eds.) 17th International Conference on Computer-Aided Verification, pp. 476\u2013490. Springer, Heidelberg (2005)"},{"key":"55_CR11","doi-asserted-by":"crossref","unstructured":"Moore, J., Lynch, T., Kaufmann, M.: A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5k86 Floating-Point Division Program. IEEE Transactions on Computers\u00a047(9) (1998)","DOI":"10.1109\/12.713311"},{"key":"55_CR12","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Park, D., Chou, A., Engler, D., Dill, D.: CMC: A Pragmatic Approach to Model Checking Real Code. In: 5th Symposium on Operating Systems Design and Implementation (December 2002)","DOI":"10.1145\/1060289.1060297"},{"key":"55_CR13","doi-asserted-by":"crossref","unstructured":"Norman, G., Shmatikov, V.: Analysis of Probabilistic Contract Signing. In: BCSFACS Formal Aspects of Security (FASec 2002) (2002)","DOI":"10.1007\/978-3-540-40981-6_9"},{"key":"55_CR14","volume-title":"16th IEEE Symposium on Logic in Computer Science","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F.: Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. In: 16th IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"55_CR15","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/s001650200018","volume":"13","author":"R. Pollack","year":"2002","unstructured":"Pollack, R.: Dependently Typed Records in Type Theory. Formal Aspects of Computing\u00a013, 386\u2013402 (2002)","journal-title":"Formal Aspects of Computing"},{"key":"55_CR16","doi-asserted-by":"crossref","unstructured":"Ruess, H., Shankar, N., Srivas, M.: Modular Verification of SRT Division. Formal Methods in System Design\u00a014(1) (1999)","DOI":"10.1023\/A:1008617612073"},{"key":"55_CR17","doi-asserted-by":"crossref","unstructured":"Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging Overconstrained Declarative Models Using Unsatisfiable Cores. In: 18th IEEE International Conference on Automated Software Engineering (2003) (received best paper award)","DOI":"10.1109\/ASE.2003.1240298"},{"issue":"2","key":"55_CR18","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/S0747-7171(02)00091-3","volume":"35","author":"M. Velev","year":"2003","unstructured":"Velev, M., Bryant, R.: Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. Journal of Symbolic Computation\u00a035(2), 73\u2013106 (2003)","journal-title":"Journal of Symbolic Computation"},{"issue":"5","key":"55_CR19","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1109\/32.588523","volume":"23","author":"C. Wang","year":"1997","unstructured":"Wang, C., Musser, D.: Dynamic Verification of C++ Generic Algorithms. IEEE Transactions on Software Engineering\u00a023(5), 314\u2013323 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"55_CR20","doi-asserted-by":"crossref","unstructured":"Westbrook, E., Stump, A.: A Language-based Approach to Functionally Correct Imperative Programming. In: 10th ACM SIGPLAN International Conference on Functional Programming (2005)","DOI":"10.1145\/1086365.1086400"},{"key":"55_CR21","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Scalable Error Detection using Boolean Satisfiability. In: Abadi, M. (ed.) Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (2005)","DOI":"10.1145\/1040305.1040334"},{"key":"55_CR22","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-30557-6_8","volume-title":"Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages","author":"D. Zhu","year":"2005","unstructured":"Zhu, D., Xi, H.: Safe Programming with Pointers through Stateful Views. In: Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages, pp. 83\u201397. Springer, Heidelberg (2005)"}],"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_55","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T03:44:26Z","timestamp":1557719066000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_55"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_55","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}