Abstract
In this paper, we present a path sensitive type system for resource usage verification. Path sensitivity is essential to model resource usage in C programs correctly and accurately. So far, most of methods to analyze this kind of property in the path sensitive way have been proposed as whole program analyses or unsound analyses. Our main contributions are as follows. First, we formalize a sound analysis for path sensitive resource usage properties in C like languages. To the best of our knowledge, it is the first sound and modular analysis for this problem. We provide the complete proof for the soundness of the type system and algorithm. Second, our analysis is modular, and we provide an inference algorithm to generate function summaries automatically. We believe that our approach suggests new insights into the design of modular analyses.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aiken, A., Fähndrich, M., Levien, R.: Better Static Memory Management: Improving Region-Based Analysis of Higher-Order Languages. In: PLDI (1995)
Ball, T., Rajamani, S.: The SLAM Project: Debugging System Software via Static Analysis. In: POPL (2002)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular Verification of Software Components in C. In: ICSE (2003)
Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Das, M., Lerner, S., Seigle, M.: ESP: Path-Sensitive Program Verification in Polynomial Time. In: PLDI (2002)
DeLine, R., Fähndrich, M.: Enforcing High-Level Protocols in Low-Level Software. In: PLDI (2001)
Dor, N., Adams, S., Das, M., Yang, Z.: Software Validation via Scalable Path-Sensitive Value Flow Analysis. In: ISSTA (2004)
Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions. In: OSDI (2000)
Fähndrich, M., DeLine, R.: Typestates for Objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465–490. Springer, Heidelberg (2004)
Field, J., Goyal, D., Ramalingam, G., Yahav, E.: Typestate Verification: Abstraction Techniques and Complexity Result. In: SAS (2003)
Flanagan, C., Abadi, M.: Object Types Against Races. In: CONCUR (1999)
Flanagan, C., Abadi, M.: Types for Safe Locking. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, p. 91. Springer, Heidelberg (1999)
Flanagan, C., Leino, K., Lillibridge, M., Nelson, G., Saxe, J., State, R.: Extended Static Checking for Java. In: PLDI (2002)
Foster, J., Terauhi, T., Aiken, A.: Flow-Sensitive Type Qualifiers. In: PLDI (2002)
Freund, S., Mitchell, J.: The Type System for Object Initialization in the Java Bytecode Language. TOPLAS 21(6), 1196–1250 (1999)
Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with BLAST. In: 10th International SPIN Workshop (2003)
Igarashi, A., Kobayashi, N.: Resource Usage Analysis. In: POPL (2002)
Kang, H.-G., Kim, Y., Han, T., Han, H.: A Path Sensitive Type System for Resource Usage Verification of C like Languages (2005), http://pllab.kaist.ac.kr/~hgkang/pruv-tm.pdf
Kobayashi, N.: Quasi-Linear Types. In: POPL (1999)
Kobayashi, N.: Time Regions and Effects for Resource Usage Analysis. In: TLDI (2003)
Laneve, C.: A Type System for JVM Threads. Theoretical Computer Science 290(1), 741–778 (2003)
Lee, O., Yang, H., Yi, K.: Inserting Safe Memory Reuse Commands into ML-like Programs. In: SAS (2003)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC (2001)
Shapiro, M., Horwitz, S.: The Effects of the Precision of Pointer Analysis. In: SAS (1997)
Smith, G.: Polymorphic Type Inference for Languages with Overloading and Subtyping. PhD thesis, Cornell University (August 1991)
SPEC. SPEC Benchmarks Suite, http://www.spec.org/
Strom, R., Yemini, S.: Typestate: A Programming Language Concept for Enhancing Software Reliability. IEEE Transactions on Software Engineering 12(1), 157–171 (1986)
Tan, G., Ou, X., Walker, D.: Enforcing Resource Usage Protocols via Scoped Methods. In: FOOL (2003)
Tofte, M., Birkedal, L.: A Region Inference Algorithm. TOPLAS 20(4), 734–767 (1998)
Walker, D., Crary, K., Morriset, G.: Typed Memory Management via Static Capabilities. TOPLAS 22(4), 701–771 (2000)
Xie, Y., Aiken, A.: Scalable Error Detection using Boolean Satisfiability. In: POPL, pp. 351–363 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kang, HG., Kim, Y., Han, T., Han, H. (2005). A Path Sensitive Type System for Resource Usage Verification of C Like Languages. In: Yi, K. (eds) Programming Languages and Systems. APLAS 2005. Lecture Notes in Computer Science, vol 3780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11575467_18
Download citation
DOI: https://doi.org/10.1007/11575467_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29735-2
Online ISBN: 978-3-540-32247-4
eBook Packages: Computer ScienceComputer Science (R0)