ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
Parametric shape analysis via 3-valued logic
Full text PdfPdf (2.29 MB)
Source Annual Symposium on Principles of Programming Languages archive
Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents
San Antonio, Texas, United States
Pages: 105 - 118  
Year of Publication: 1999
ISBN:1-58113-095-3
Authors
Mooly Sagiv  Dept. of Comp. Sci., Tel-Aviv Univ., Tel-Aviv 69978, Israel
Thomas Reps  Comp. Sci. Dept., Univ. of Wisconsin, 1210 W. Dayton St., Madison, WI
Reinhard Wilhelm  Fachbereich 14 Informatik, Univ. des Saarlandes, 66123 Saarbrücken; Germany
Sponsors
SIGPLAN: ACM Special Interest Group on Programming Languages
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
Publisher
ACM  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): 19,   Downloads (12 Months): 75,   Citation Count: 58
Additional Information:

references   cited by   index terms   collaborative colleagues  

Tools and Actions: Request Permissions Request Permissions    Review this Article  
DOI Bookmark: Use this link to bookmark this Article: http://doi.acm.org/10.1145/292540.292552
What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

 
1
U. Assmann and M. Weinhardt. Interprocedural heap analysis for parallelizing imperative programs. In W. K. Giloi, S. J~ihnichen, and B. D. Shriver, editors, Programming Models For Massively Parallel Computers, pages 74-82, Washington, DC, September 1993. IEEE Press.
2
David R. Chase , Mark Wegman , F. Kenneth Zadeck, Analysis of pointers and structures, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.296-310, June 1990, White Plains, New York, United States
3
Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas  [doi>10.1145/567752.567778]
 
4
A. Deutsch. A storeless model for aliasing and its abstractions using finite representations of right-regular equivalence relations. In IEEE International Conference on Computer Languages, pages 2-13, Washington, DC, 1992. IEEE Press.
5
Alain Deutsch, Interprocedural may-alias analysis for pointers: beyond k-limiting, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.230-241, June 20-24, 1994, Orlando, Florida, United States
 
6
Laurie Jane Hendren, Parallelizing programs with recursive data structures, Cornell University, Ithaca, NY, 1990
7
Laurie J. Hendren , Joseph Hummell , Alexandru Nicolau, Abstractions for recursive pointer data structures: improving the analysis and transformation of imperative programs, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.249-260, June 15-19, 1992, San Francisco, California, United States
 
8
L. J. Hendren , A. Nicolau, Parallelizing Programs with Recursive Data Structures, IEEE Transactions on Parallel and Distributed Systems, v.1 n.1, p.35-47, January 1990  [doi>10.1109/71.80123]
 
9
C.A.R. Hoare. Recursive data structures. Int. d. of Comp. and Inf. Sci., 4(2):105-132, 1975.
10
S. Horwitz , P. Pfeiffer , T. Reps, Dependence analysis for pointer variables, Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation, p.28-40, June 19-23, 1989, Portland, Oregon, United States
 
11
N.D. Jones and S.S. Muchnick. Flow analysis and optimization of Lisp-like structures. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 4, pages 102-131. Prentice-Hall, Englewood Cliffs, NJ, 1981.
12
Neil D. Jones , Steven S. Muchnick, A flexible approach to interprocedural data flow analysis and programs with recursive data structures, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.66-74, January 25-27, 1982, Albuquerque, Mexico  [doi>10.1145/582153.582161]
 
13
S.C. Kleene. Introduction to Metamathematics. North- Holland, second edition, 1987.
14
William Landi , Barbara G. Ryder, Pointer-induced aliasing: a problem taxonomy, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.93-103, January 21-23, 1991, Orlando, Florida, United States  [doi>10.1145/99583.99599]
15
J. R. Larus , P. N. Hilfinger, Detecting conflicts between structure accesses, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.24-31, June 20-24, 1988, Atlanta, Georgia, United States
 
16
John Plevyak , Andrew A. Chien , Vijay Karamcheti, Analysis of Dynamic Structures for Efficient Parallel Execution, Proceedings of the 6th International Workshop on Languages and Compilers for Parallel Computing, p.37-56, August 12-14, 1993
17
Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.16-31, January 21-24, 1996, St. Petersburg Beach, Florida, United States  [doi>10.1145/237721.237725]
 
18
M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. Tech. Rep. TR-1383, Comp. Sci. Dept., Univ. of Wisconsin, Madison, WI, July 1998. Available at "http://www.cs.wisc.edu/wpis/papers/parametric.ps".
19
Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.1-50, Jan. 1998  [doi>10.1145/271510.271517]
 
20
S. Sagiv, N. Francez, M. Rodeh, and R. Wilhelm. A logic-based approach to data flow analysis problems. Acta Inf., 35(6):457- 504, June 1998.
 
21
Jan Stransky, A lattice for abstract interpretation of dynamic (LISP-like) structures, Information and Computation, v.101 n.1, p.70-102, Nov. 1992  [doi>10.1016/0890-5401(92)90076-R]
 
22
Edward Yan-Bing Wang , Paul N. Hilfinger, Analysis of recursive types in an imperative language, 1994

CITED BY  58
Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, ACM SIGPLAN Notices, v.36 n.5, p.59-69, May 2001
Samin S. Ishtiaq , Peter W. O'Hearn, BI as an assertion language for mutable data structures, ACM SIGPLAN Notices, v.36 n.3, p.14-26, March 2001
Anders Møller , Michael I. Schwartzbach, The pointer assertion logic engine, ACM SIGPLAN Notices, v.36 n.5, p.221-231, May 2001
Marius Bozga , Radu Iosif , Yassine Laknech, Storeless semantics and alias logic, ACM SIGPLAN Notices, v.38 n.10, p.55-65, October 2003
Thomas Ball , Sriram K. Rajamani, Bebop: a path-sensitive interprocedural dataflow engine, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.97-103, June 2001, Snowbird, Utah, United States
Hanne Riis Nielson , Flemming Nielson, Shape analysis for mobile ambients, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.142-154, January 19-21, 2000, Boston, MA, USA
Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002
Manuel Fahndrich , Robert DeLine, Adoption and focus: practical linear types for imperative programming, ACM SIGPLAN Notices, v.37 n.5, May 2002
Michael Hind, Pointer analysis: haven't we solved this problem yet?, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.54-61, June 2001, Snowbird, Utah, United States
G. Ramalingam , Alex Warshavsky , John Field , Deepak Goyal , Mooly Sagiv, Deriving specialized program analyses for certifying component-client conformance, ACM SIGPLAN Notices, v.37 n.5, May 2002
Manuvir Das, Unification-based pointer analysis with directional assignments, ACM SIGPLAN Notices, v.35 n.5, p.35-46, May 2000
Tal Lev-Ami , Thomas Reps , Mooly Sagiv , Reinhard Wilhelm, Putting static analysis to work for verification: A case study, ACM SIGSOFT Software Engineering Notes, v.25 n.5, p.26-38, Sept. 2000
Shai Rubin , Rastislav Bodík , Trishul Chilimbi, An efficient profile-analysis framework for data-layout optimizations, ACM SIGPLAN Notices, v.37 n.1, p.140-153, Jan. 2002
Viktor Kuncak , Patrick Lam , Martin Rinard, Role analysis, ACM SIGPLAN Notices, v.37 n.1, p.17-32, Jan. 2002
Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, ACM SIGSOFT Software Engineering Notes, v.25 n.5, p.14-25, Sept. 2000
Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, ACM SIGPLAN Notices, v.36 n.5, p.203-213, May 2001
Steve Easterbrook , Marsha Chechik , Benet Devereux , Arie Gurfinkel , Albert Lai , Victor Petrovykh , Anya Tafliovich , Christopher Thompson-Walsh, χChek: a model checker for multi-valued reasoning, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
Beatrix Braune , Reinhard Wilhelm, Focusing in Algorithm Explanation, IEEE Transactions on Visualization and Computer Graphics, v.6 n.1, p.1-7, January 2000
Eran Yahav, Verifying safety properties of concurrent Java programs using 3-valued logic, ACM SIGPLAN Notices, v.36 n.3, p.27-40, March 2001
Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001
Marsha Chechik , Benet Devereux , Arie Gurfinkel, Model-checking infinite state-space systems with fine-grained abstractions using SPIN, Proceedings of the 8th international SPIN workshop on Model checking of software, p.16-36, May 2001, Toronto, Ontario, Canada
Marsha Chechik , Benet Devereux , Steve Easterbrook , Arie Gurfinkel, Multi-valued symbolic model-checking, ACM Transactions on Software Engineering and Methodology (TOSEM), v.12 n.4, p.371-408, October 2003
Nurit Dor , Stephen Adams , Manuvir Das , Zhe Yang, Software validation via scalable path-sensitive value flow analysis, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
Brian Hackett , Radu Rugina, Region-based shape analysis with tracked locations, ACM SIGPLAN Notices, v.40 n.1, p.310-323, January 2005
V. Benjamin Livshits , Monica S. Lam, Tracking pointers with path and context sensitivity for bug detection in C programs, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003
Dierk Johannes , Raimund Seidel , Reinhard Wilhelm, Algorithm animation using shape analysis: visualising abstract executions, Proceedings of the 2005 ACM symposium on Software visualization, May 14-15, 2005, St. Louis, Missouri
Hanne Riis Nielson , Flemming Nielson, Flow logic: a multi-paradigmatic approach to static analysis, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
Francisco Corbera , Rafael Asenjo , Emilio L. Zapata, A Framework to Capture Dynamic Data Structures in Pointer-Based Codes, IEEE Transactions on Parallel and Distributed Systems, v.15 n.2, p.151-166, February 2004
Edwin Westbrook , Aaron Stump , Ian Wehrman, A language-based approach to functionally correct imperative programming, ACM SIGPLAN Notices, v.40 n.9, September 2005
Cormac Flanagan , Stephen N. Freund , Shaz Qadeer , Sanjit A. Seshia, Modular verification of multithreaded programs, Theoretical Computer Science, v.338 n.1-3, p.153-183, 10 June 2005
Shuvendu K. Lahiri , Shaz Qadeer, Verifying properties of well-founded linked lists, ACM SIGPLAN Notices, v.41 n.1, p.115-126, January 2006
Wei-Ngan Chin , Siau-Cheng Khoo , Shengchao Qin , Corneliu Popeea , Huu Hai Nguyen, Verifying safety policies with size properties and alias controls, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA
Edmund Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM (JACM), v.50 n.5, p.752-794, September 2003
Jeffrey Fischer , Ranjit Jhala , Rupak Majumdar, Joining dataflow with predicates, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
Oscar Plata , Rafael Asenjo , Eladio Gutiérrez , Francisco Corbera , Angeles Navarro , Emilio L. Zapata, On the parallelization of irregular and dynamic programs, Parallel Computing, v.31 n.6, p.544-562, June 2005
Stephen Fink , Eran Yahav , Nurit Dor , G. Ramalingam , Emmanuel Geay, Effective typestate verification in the presence of aliasing, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
Greta Yorsh , Thomas Reps , Mooly Sagiv , Reinhard Wilhelm, Logical characterizations of heap abstractions, ACM Transactions on Computational Logic (TOCL), v.8 n.1, p.5-es, January 2007
Jeffrey S. Foster , Robert Johnson , John Kodumal , Alex Aiken, Flow-insensitive type qualifiers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.6, p.1035-1087, November 2006
David A. Schmidt, A calculus of logical relations for over- and underapproximating static analyses, Science of Computer Programming, v.64 n.1, p.29-53, January, 2007
Harvey Tuch , Gerwin Klein , Michael Norrish, Types, bytes, and separation logic, ACM SIGPLAN Notices, v.42 n.1, January 2007
V. Benjamin Livshits , Monica S. Lam, Finding security vulnerabilities in java applications with static analysis, Proceedings of the 14th conference on USENIX Security Symposium, p.18-18, July 31-August 05, 2005, Baltimore, MD
Martin Hirzel , Daniel Von Dincklage , Amer Diwan , Michael Hind, Fast online pointer analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.2, p.11-es, April 2007
Sigmund Cherem , Lonnie Princehouse , Radu Rugina, Practical memory leak detection using guarded value-flow analysis, ACM SIGPLAN Notices, v.42 n.6, June 2007
Mark Marron , Darko Stefanovic , Manuel Hermenegildo , Deepak Kapur, Heap analysis in the presence of collection libraries, Proceedings of the 7th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.31-36, June 13-14, 2007, San Diego, California, USA
Michael R. A. Huth , Radha Jagadeesan , David A. Schmidt, A domain equation for refinement of partial systems, Mathematical Structures in Computer Science, v.14 n.4, p.469-505, August 2004
Carlo Ghezzi , Andrea Mocci , Mattia Monga, Efficient recovery of algebraic specifications for stateful components, Ninth international workshop on Principles of software evolution: in conjunction with the 6th ESEC/FSE joint meeting, September 03-04, 2007, Dubrovnik, Croatia
Marsha Chechik , Wei Ding, Lightweight Reasoning about Program Correctness, Information Systems Frontiers, v.4 n.4, p.363-377, December 2002
Altaf Hussain , Michael Huth, On model checking multiple hybrid views, Theoretical Computer Science, v.404 n.3, p.186-201, September, 2008
Jacinta Townley , Joseph Manning , Michel Schellekens, Sorting Algorithms in MOQA, Electronic Notes in Theoretical Computer Science (ENTCS), 225, p.391-404, January, 2009
Sascha A. Parduhn , Raimund Seidel , Reinhard Wilhelm, Algorithm visualization using concrete and abstract shape graphs, Proceedings of the 4th ACM symposium on Software visuallization, September 16-17, 2008, Ammersee, Germany
Tova Milo , Daniel Deutch, Querying and monitoring distributed business processes, Proceedings of the VLDB Endowment, v.1 n.2, August 2008
Mark Marron , Mario Méndez-Lojo , Manuel Hermenegildo , Darko Stefanovic , Deepak Kapur, Sharing analysis of arrays, collections, and recursive structures, Proceedings of the 8th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, November 09-10, 2008, Atlanta, Georgia
Marwan Abi-Antoun , Jonathan Aldrich, Static extraction of sound hierarchical runtime object graphs, Proceedings of the 4th international workshop on Types in language design and implementation, January 24-24, 2009, Savannah, GA, USA
Edward E. Aftandilian , Samuel Z. Guyer, GC assertions: using the garbage collector to check heap properties, ACM SIGPLAN Notices, v.44 n.6, June 2009
Mark Marron , Deepak Kapur , Manuel Hermenegildo, Identification of logically related heap regions, Proceedings of the 2009 international symposium on Memory management, June 19-20, 2009, Dublin, Ireland
Harvey Tuch, Formal Verification of C Systems Code, Journal of Automated Reasoning, v.42 n.2-4, p.125-187, April 2009
María Del Mar Gallardo , Pedro Merino , David Sanán, Model Checking Dynamic Memory Allocation in Operating Systems, Journal of Automated Reasoning, v.42 n.2-4, p.229-264, April 2009
Hanne Riis Nielson , Flemming Nielson, A monotone framework for CCS, Computer Languages, Systems and Structures, v.35 n.4, p.365-394, December, 2009

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Logic programming


General Terms:
Algorithms, Measurement

Collaborative Colleagues:
Mooly Sagiv: colleagues
Thomas Reps: colleagues
Reinhard Wilhelm: colleagues

The ACM Portal is published by the Association for Computing Machinery. Copyright © 2009 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player