Abstract
Today’s software does not come with meaningful guarantees. This position paper explores why this is the case, suggests societal and technical impediments to more dependable software, and considers what realistic, meaningful guarantees for software would be like and how to achieve them.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Černý, P., Madhusudan, P., Nam, W.: Synthesis of Interface Specifications for Java classes. In: Proceedings of the ACM Symposium on Principles of Programming Languages (2005)
Ammons, G., Bodik, R., Larus, J.R.: Mining Specifications. In: Proceedings of the ACM Symposium on Principles of Programming Languages (January 2002)
Anderson, R.: Economics and Security Resource Page, http://www.cl.cam.ac.uk/users/rja14/econsec.html
Camp, L.J., Lewis, S. (eds.): Economics of Information Security, September 2004. Kluwer Academic Publishers, Dordrecht (2004)
Chen, H., Dean, D., Wagner, D.: Model Checking One Million Lines of C Code. In: Proceedings of the 11th Annual Network and Distributed System Security Symposium (NDSS) (February 2004)
CS150: Computer Science from Ada and Euclid to Quantum Computing and the World Wide Web. University of Virginia Course, http://www.cs.virginia.edu/cs150
CS201j: Engineering Software. University of Virginia, http://www.cs.virginia.edu/cs201j
CS655: Graduate Programming Languages. University of Virginia Course. (Spring, 2000), http://www.cs.virginia.edu/evans/cs655-S00/mocktrial/
Cook, J.E., Du, Z., Liu, C., Wolf, A.L.: Discovering Models of Behavior for Concurrent Workflows. Computers in Industry 53(3), 297–319 (2004)
Das, M., Lerner, S., Seigle, M.: ESP: Path-Sensitive Program Verification In Polynomial Time. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (June 2002)
Demsky, B., Rinard, M.: Data Structure Repair Using Goal-Directed Reasoning. In: Proceedings of the 2005 International Conference on Software Engineering (May 2005)
Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking System Rules Using System-Specific Programmer-Written Compiler Extensions. In: Symposium on Operating Systems Design and Implementation (October 2000)
Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically Discovering Likely Program Invariants to Support Program Evolution. IEEE Transactions on Software Engineering (February 2001)
Evans, D.: Static Detection of Dynamic Memory Errors. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (May 1996)
Evans, D., Peck, M.: Simulating Critical Software Development. University of Virginia Computer Science Technical Report, UVA-CS-TR2004-04 (February 2004)
Evans, L.: Traffic Safety. Science Serving Society Press (2004), http://scienceservingsociety.com/traffic-safety.htm
Evans, L.: Personal communication (April 2005)
Gates, B.: Trustworthy Computing Initiative (memo to all Microsoft employees) (January 15, 2002)
Howard, M., Pincus, J., Wing, J.M.: Measuring Relative Attack Surfaces. In: Proceedings of Workshop on Advanced Developments in Software and Systems Security, Taipei (December 2003)
Larochelle, D., Evans, D.: Statically Detecting Likely Buffer Overflow Vulnerabilities. In: USENIX Security Symposium (August 2001)
Microsoft Corporation. Trustworthy Computing, http://www.microsoft.com/twc
Musuvathi, M., Park, D., Chou, A., Engler, D.R., Dill, D.L.: CMC: A Pragmatic Approach to Model Checking Real Code. In: Proceedings of the Fifth Symposium on Operating Systems Design and Implementation (December 2002)
Ozment, A.: Bug Auctions: Vulnerability Markets Reconsidered. In: Workshop on Economics and Information Security (May 2004)
Rinard, M.: Acceptability-Oriented Computing. In: ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications Companion (OOPSLA 2003 Companion) Onwards! Session, California (October 2003)
Rinard, M., Cadar, C., Dumitran, D., Roy, D.M., Leu, T., Beebee Jr, W.S.: Enhancing Server Availability and Security Through Failure-Oblivious Computing. In: Proceedings of the 6th Symposium on Operating Systems Design and Implementation (December 2004)
Swift, M., Annalamai, M., Bershad, B., Levy, H.: Recovering Device Drivers. In: Proceedings of the 6th Symposium on Operating Systems Design and Implementation (December 2004)
Yang, J., Evans, D.: Dynamically Inferring Temporal Properties. In: ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (June 2004)
Yang, J., Evans, D.: Automatically Inferring Temporal Properties for Program Evolution. In: 15th IEEE International Symposium on Software Reliability Engineering (November 2004)
Yang, J., Evans, D., Bhardwaj, D., Bhat, T., Das, M.: Perracotta: Mining Temporal API Rules from Imperfect Traces. In: 28th International Conference in Software Engineering (May 2006)
Weimer, W., Necula, G.: Mining Temporal Specifications for Error Detection. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 461–476. Springer, Heidelberg (2005)
Whaley, J., Martin, M.C., Lam, M.S.: Automatic extraction of object-oriented component interfaces. In: International Symposium on Software Testing and Analysis (July 2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Evans, D. (2008). Toasters, Seat Belts, and Inferring Program Properties. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_38
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)