Region-based shape analysis with tracked locations. (English) Zbl 1369.68140
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’05, Long Beach, CA, USA, January 12–14, 2005. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-830-X). 310-323 (2005).
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68N20 | Theory of compilers and interpreters |
| 68P05 | Data structures |
References:
| [1] | S. Amarasinghe, J. Anderson, M. Lam, and C. Tseng. The SUIF compiler for scalable parallel machines. In Proceedings of the Eighth SIAM Conference on Parallel Processing for Scientific Computing, San Francisco, CA, February 1995.]] |
| [2] | T. Ball, R. Majumdar, T. Millstein, and S. Rajamani. Automatic predicate abstraction of C programs. In Proceedings of the SIGPLAN ’01 Conference on Program Language Design and Implementation, Snowbird, UT, June 2001.]] 10.1145/378795.378846 |
| [3] | T. Ball and S. Rajamani. The SLAM project: Debugging system software via static analysis. In Proceedings of the 29th Annual ACM Symposium on the Principles of Programming Languages, Portland, OR, January 2002.]] 10.1145/503272.503274 |
| [4] | W. Bush, J. Pincus, and D. Sielaff. A static analyzer for finding dynamic programming errors. Software – Practice and Experience, 30(7):775-802, August 2000.]] 10.1002/(SICI)1097-024X(200006)30:7 · Zbl 1009.68852 |
| [5] | S. Chong and R. Rugina. Static analysis of accessed regions in recursive data structures. In Proceedings of the 10th International Static Analysis Symposium, San Diego, CA, June 2003.]] |
| [6] | M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In Proceedings of the SIGPLAN ’02 Conference on Program Language Design and Implementation, Berlin, Germany, June 2002.]] 10.1145/512529.512538 |
| [7] | R. DeLine and M. Fahndrich. Enforcing high-level protocols in low-level software. In Proceedings of the SIGPLAN ’01 Conference on Program Language Design and Implementation, Snowbird, UT, June 2001.]] 10.1145/378795.378811 |
| [8] | N. Dor, M. Rodeh, and M. Sagiv. Checking cleanness in linked lists. In Proceedings of the 7th International Static Analysis Symposium, Santa Barbara, CA, July 2000.]] |
| [9] | D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the SIGPLAN ’02 Conference on Program Language Design and Implementation, Berlin, Germany, June 2002.]] |
| [10] | M. Fahndrich, J. Rehof, and M. Das. Scalable context-sensitive flow analysis using instantiation constraints. In Proceedings of the SIGPLAN ’00 Conference on Program Language Design and Implementation, Vancouver, Canada, June 2000.]] 10.1145/349299.349332 |
| [11] | R. Ghiya and L. Hendren. Is is a tree, a DAG or a cyclic graph? a shape analysis for heap-directed pointers in C. In Proceedings of the 23rd Annual ACM Symposium on the Principles of Programming Languages, St. Petersburg Beach, FL, January 1996.]] 10.1145/237721.237724 |
| [12] | B. Hackett and R. Rugina. Region-based shape analysis with tracked locations. Technical Report TR2004-1968, Cornell University, October 2004.]] |
| [13] | R. Hastings and B. Joyce. Purify: Fast detection of memory leaks and access errors. In Proceedings of the 1992 Winter Usenix Conference, January 1992.]] |
| [14] | M. Hauswirth and T. Chilimbi. Low-overhead memory leak detection using adaptive statistical profiling. In Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems, Boston, MA, October 2004.]] 10.1145/1024393.1024412 |
| [15] | D. Heine and M. Lam. A practical flow-sensitive and context-sensitive C and C++ memory leak detector. In Proceedings of the SIGPLAN ’03 Conference on Program Language Design and Implementation, San Diego, CA, June 2003.]] 10.1145/781131.781150 |
| [16] | N. Heintze and O. Tardieu. Demand-driven pointer analysis. In Proceedings of the SIGPLAN ’01 Conference on Program Language Design and Implementation, Snowbird, UT, June 2001.]] 10.1145/378795.378802 |
| [17] | L. Hendren, J. Hummel, and A. Nicolau. A general data dependence test for dynamic, pointer-based data structures. In Proceedings of the SIGPLAN ’94 Conference on Program Language Design and Implementation, Orlando, FL, June 1994.]] 10.1145/178243.178262 |
| [18] | L. Hendren and A. Nicolau. Parallelizing programs with recursive data structures. IEEE Transactions on Parallel and Distributed Systems, 1(1):35-47, January 1990.]] 10.1109/71.80123 |
| [19] | S. Ishtiaq and P. O’Hearn. BI as an assertion language for mutable data structures. In Proceedings of the 28th Annual ACM Symposium on the Principles of Programming Languages, London, UK, January 2001.]] 10.1145/360204.375719 · Zbl 1323.68077 |
| [20] | B. Jeannet, A. Loginov, T. Reps, and M. Sagiv. A relational approach to interprocedural shape analysis. In Proceedings of the 11th International Static Analysis Symposium, Verona, Italy, August 2004.]] · Zbl 1104.68416 |
| [21] | V. Kuncak, P. Lam, and M. Rinard. Role analysis. In Proceedings of the 29th Annual ACM Symposium on the Principles of Programming Languages, Portland, OR, January 2002.]] 10.1145/503272.503276 · Zbl 1323.68378 |
| [22] | T. Lev-ami, T. Reps, M. Sagiv, and R. Wilhelm. Putting static analysis to work for verification: A case study. In 2000 International Symposium on Software Testing and Analysis, August 2000.]] 10.1145/347324.348031 |
| [23] | T. Lev-Ami and M. Sagiv. TVLA: A system for implementing static analyses. In Proceedings of the 7th International Static Analysis Symposium, Santa Barbara, CA, July 2000.]] |
| [24] | D. Liang and M.J. Harrold. Efficient points-to analysis for whole-program analysis. In Proceedings of the ACM SIGSOFT ’99 Symposium on the Foundations of Software Engineering, Toulouse,France, September 1999.]] |
| [25] | G. Necula, S. McPeak, and W. Weimer. CCured: type-safe retrofitting of legacy code. In Proceedings of the 29th Annual ACM Symposium on the Principles of Programming Languages, Portland, OR, January 2002.]] 10.1145/503272.503286 · Zbl 1323.68382 |
| [26] | P. O’Hearn, H. Yang, and J. Reynolds. Separation and information hiding. In Proceedings of the 31th Annual ACM Symposium on the Principles of Programming Languages, Venice, Italy, January 2004.]] 10.1145/964001.964024 · Zbl 1325.68069 |
| [27] | J. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark, July 2002.]] |
| [28] | N. Rinetzky and M. Sagiv. Interprocedural shape analysis for recursive programs. In Proceedings of the 2001 International Conference on Compiler Construction, Genova, Italy, April 2001.]] · Zbl 0977.68688 |
| [29] | M. Sagiv, T. Reps, and R. Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems, 20(1):1-50, January 1998.]] 10.1145/271510.271517 |
| [30] | M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In Proceedings of the 26th Annual ACM Symposium on the Principles of Programming Languages, San Antonio, TX, January 1999.]] 10.1145/292540.292552 |
| [31] | M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems, 24(3), May 2002.]] 10.1145/514188.514190 |
| [32] | Bjarne Steensgaard. Points-to analysis in almost linear time. In Proceedings of the 23rd Annual ACM Symposium on the Principles of Programming Languages, St. Petersburg Beach, FL, January 1996.]] 10.1145/237721.237727 |
| [33] | F. Vivien and M. Rinard. Incrementalized pointer and escape analysis. In Proceedings of the SIGPLAN ’01 Conference on Program Language Design and Implementation, Snowbird, UT, June 2001.]] 10.1145/378795.378804 |
| [34] | R. Wilhelm, M. Sagiv, and T. Reps. Shape analysis. In Proceedings of the 2000 International Conference on Compiler Construction, Berlin, Germany, April 2000.]] |
| [35] | E. Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proceedings of the 28th Annual ACM Symposium on the Principles of Programming Languages, London, UK, January 2001.]] 10.1145/360204.360206 · Zbl 1323.68183 |
| [36] | E. Yahav and G. Ramalingam. Verifying safety properties using separation and heterogeneous abstractions. In Proceedings of the SIGPLAN ’04 Conference on Program Language Design and Implementation, Washington, DC, June 2004.]] 10.1145/996841.996846 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
