
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Viktor Kuncak, Patrick Lam, Karen Zee, Martin C. Rinard, "Modular Pluggable Analyses for Data Structure Consistency," IEEE Transactions on Software Engineering, vol. 32, no. 12, pp. 9881005, December, 2006.  
BibTex  x  
@article{ 10.1109/TSE.2006.125, author = {Viktor Kuncak and Patrick Lam and Karen Zee and Martin C. Rinard}, title = {Modular Pluggable Analyses for Data Structure Consistency}, journal ={IEEE Transactions on Software Engineering}, volume = {32}, number = {12}, issn = {00985589}, year = {2006}, pages = {9881005}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2006.125}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Modular Pluggable Analyses for Data Structure Consistency IS  12 SN  00985589 SP988 EP1005 EPD  9881005 A1  Viktor Kuncak, A1  Patrick Lam, A1  Karen Zee, A1  Martin C. Rinard, PY  2006 KW  Typestate KW  data structure KW  invariant KW  program analysis KW  program verification KW  shape analysis KW  formal methods KW  programming language design. VL  32 JA  IEEE Transactions on Software Engineering ER   
[1] A. Møller and M.I. Schwartzbach, “The Pointer Assertion Logic Engine,” Programming Language Design and Implementation, 2001.
[2] M. Sagiv, T. Reps, and R. Wilhelm, “Parametric Shape Analysis via 3Valued Logic,” ACM Trans. Program Languages and Systems, vol. 24, no. 3, pp. 217298, 2002.
[3] T. Ball, R. Majumdar, T. Millstein, and S.K. Rajamani, “Automatic Predicate Abstraction of C programs,” Proc. ACM Programming Language Design and Implementation Conf. (PLDI), 2001.
[4] T.A. Henzinger, R. Jhala, R. Majumdar, and K.L. McMillan, “Abstractions from Proofs,” Proc. 31st Symp. Principles of Programming Languages, 2004.
[5] S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith, “Modular Verification of Software Components in C,” Proc. Int'l Conf. Software Eng. (ICSE '03), 2003.
[6] N. Bjørner, A. Browne, E. Chang, M. Colón, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe, “STeP: DeductiveAlgorithmic Verification of Reactive and RealTime systems,” Proc. Eighth Conf. ComputerAided Verification, vol. 1102, pp. 415418, 1996.
[7] M. Musuvathi, D.Y. Park, A. Chou, D.R. Engler, and D.L. Dill, “CMC: A Pragmatic Approach to Model Checking Real Code,” Proc. Symp. Operating Systems Design and Implementation (OSDI '02), 2002.
[8] C. Flanagan, K.R.M. Leino, M. Lilibridge, G. Nelson, J.B. Saxe, and R. Stata, “Extended Static Checking for Java,” Proc. ACM Conf. Programming Language Design and Implementation (PLDI), 2002.
[9] R.E. Strom and S. Yemini, “Typestate: A Programming Language Concept for Enhancing Software Reliability,” IEEE Trans. Software Eng., vol. 12, no. 1, Jan. 1986.
[10] R. DeLine and M. Fähndrich, “Enforcing HighLevel Protocols in LowLevel Software,” Proc. ACM Programming Language Design and Implementation Conf. (PLDI), 2001.
[11] M. Fähndrich and K.R.M. Leino, “Heap Monotonic Typestates,” Proc. Int'l Workshop Aliasing, Confinement and Ownership in ObjectOriented Programming (IWACO), 2003.
[12] J. Field, D. Goyal, G. Ramalingam, and E. Yahav, “Typestate Verification: Abstraction Techniques and Complexity Results,” Proc. Int'l Symp. Static Analysis, 2003.
[13] M. Fahndrich and R. DeLine, “Adoption and Focus: Practical Linear Types for Imperative Programming,” Proc. ACM Programming Language Design and Implementation Conf. (PLDI), 2002.
[14] V. Kuncak, P. Lam, and M. Rinard, “Role Analysis,” Proc. Ann. ACM Symp. Principles of Programming Languages (POPL), 2002.
[15] P. Lam, V. Kuncak, and M. Rinard, “On Our Experience with Modular Pluggable Analyses,” Technical Report 965, Computer Science and Artifical Intelligence Laboratory (CSAIL), Massachusetts Inst. of Tech nology, Sept. 2004.
[16] P. Lam, V. Kuncak, and M. Rinard, “Hob: A Tool for Verifying Data Structure Consistency,” Proc. 14th Int'l Conf. Compiler Construction, tool demo, Apr. 2005.
[17] P. Lam, V. Kuncak, and M. Rinard, “Generalized Typestate Checking for Data Structure Consistency,” Proc. Sixth Int'l Conf. Verification, Model Checking and Abstract Interpretation, 2005.
[18] T. Nipkow, L.C. Paulson, and M. Wenzel, “Isabelle/HOL: A Proof Assistant for HigherOrder Logic,” Lecture Notes in Computer Science, vol. 2283. 2002.
[19] T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard, “Field Constraint Analysis,” Proc. Int'l Conf. Verification, Model Checking, and Abstract Interpretation, 2006.
[20] A. Podelski and T. Wies, “Boolean Heaps,” Proc. Int'l Static Analysis Symp., 2005.
[21] K. Zee, P. Lam, V. Kuncak, and M. Rinard, “Combining Theorem Proving with Static Analysis for Data Structure Consistency,” Proc. Int'l Workshop Software Verification and Validation (SVV '04), Nov. 2004.
[22] T. Wies, V. Kuncak, K. Zee, A. Podelski, and M. Rinard, “On Verifying Complex Properties Using Symbolic Shape Analysis,” Technical Report MPII200621, MaxPlanck Inst. for Computer Science, 2006
[23] P. Lam, V. Kuncak, and M. Rinard, “CrossCutting Techniques in Program Specification and Analysis,” Proc. Fourth Int'l Conf. AspectOriented Software Development (AOSD '05), 2005.
[24] E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns. Elements of Reusable ObjectOriented Software. AddisonWesley, 1994.
[25] J.R. Büchi, “Weak SecondOrder Arithmetic and Finite Automata,” Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, vol. 6, pp. 6692, 1960.
[26] L. Loewenheim, “Über Mögligkeiten im Relativkalkül,” Mathematische Annalen, vol. 76, pp. 228251, 1915.
[27] D. Jackson, I. Shlyakhter, and M. Sridharan, “A Micromodularity Mechanism,” Proc. ACM SIGSOFT Conf. Foundations of Software Eng./European Software Eng. Conf. (FSE/ESEC '01), 2001.
[28] A. Borgida, J. Mylopoulos, and R. Reiter, “On the Frame Problem in Procedure Specifications,” IEEE Trans. Software Eng., vol. 21, no. 10, pp. 785798, Oct. 1995.
[29] D. Kozen, “Complexity of Boolean Algebras,” Theoretical Computer Science, vol. 10, pp. 221247, 1980.
[30] B. Liskov and J. Guttag, Program Development in Java. AddisonWesley, 2001.
[31] H. Jifeng, C.A.R. Hoare, and J.W. Sanders, “Data Refinement Refined,” Proc. European Symp. Programming (ESOP '86), 1986.
[32] P. Lam, V. Kuncak, K. Zee, and M. Rinard, “Set Interfaces for Generalized Typestate and Data Structure Consistency Verification,” Theoretical Computer Science, submitted.
[33] N. Klarlund and M.I. Schwartzbach, “Graph Types,” Proc. 20th ACM Symp. Principles of Programming Languages (POPL), 1993.
[34] J.W. Thatcher and J.B. Wright, “Generalized Finite Automata Theory with an Application to a Decision Problem of SecondOrder Logic,” Math. Systems Theory, vol. 2, no. 1, pp. 5781, Aug. 1968.
[35] N. Klarlund, A. Møller, and M.I. Schwartzbach, “MONA Implementation Secrets,” Proc. Fifth Int'l Conf. Implementation and Application of Automata, LNCS, 2000.
[36] N. Klarlund and A. Møller, MONA Version 1.4 User Manual, BRICS Notes Series NS011, Dept. of Computer Science, Univ. of Aarhus, Jan. 2001.
[37] L. Stockmeyer and A.R. Meyer, “Cosmological Lower Bound on the Circuit Complexity of a Small Problem in Logic,” J. ACM, vol. 49, no. 6, pp. 753784, 2002.
[38] E.W. Dijkstra, A Discipline of Programming. Prentice Hall, 1976.
[39] C. Flanagan and J.B. Saxe, “Avoiding Exponential Explosion: Generating Compact Verification Conditions,” Proc. 20th ACM Symp. Principles of Programming Languages (POPL), 2001.
[40] P. Lam, V. Kuncak, and M. Rinard, “Generalized Typestate Checking Using Set Interfaces and Pluggable Analyses,” SIGPLAN Notices, vol. 39, pp. 4655, Mar. 2004.
[41] P. Cousot and R. Cousot, “Systematic Design of Program Analysis Frameworks,” Proc. 20th ACM Symp. Principles of Programming Languages (POPL), pp. 269282, 1979.
[42] R.E. Strom and D.M. Yellin, “Extending Typestate Checking Using Conditional Liveness Analysis,” IEEE Trans. Software Eng., vol. 19, no. 5, May 1993.
[43] K. Bierhoff and J. Aldrich, “Lightweight Object Specification with Typestates,” Proc. European Software Eng. Conf./ACM SIGSOFT Symp. Foundations of Software Eng. (ESECFSE '05), pp. 217226, Sept. 2005.
[44] V. Kuncak, “Modular Data Structure Verification,” PhD dissertation, Massachusetts Inst. of Technology, to appear, 2007.
[45] V. Kuncak, H.H. Nguyen, and M. Rinard, “An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic,” Proc. 20th Int'l Conf. Automated Deduction (CADE 20), July 2005.
[46] C.H. Papadimitriou, Computational Complexity. AddisonWesley, 1994.
[47] V. Kuncak and M. Rinard, “An Overview of the Jahob Analysis System: Project Goals and Current Status,” Proc. NSF Next Generation Software Workshop, 2006.
[48] S. Drossopoulou, F. Damiani, M. DezaniCiancaglini, and P. Giannini, “Fickle: Dynamic Object ReClassification,” Proc. 15th European Conf. ObjectOriented Programming (ECOOP), pp.130149, 2001.
[49] S. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay, “Effective Typestate Verification in the Presence of Aliasing,” Proc. Int'l Symp. Software Testing and Analysis (ISSTA '06), 2006.
[50] T. Skolem, “Untersuchungen über die Axiome des Klassenkalküls and über ‘Produktations und Summationsprobleme,’ welche gewisse Klassen von Aussagen betreffen,” Skrifter utgit av Vidnskapsselskapet i Kristiania, I. klasse, no. 3, 1919.
[51] V. Kuncak, H.H. Nguyen, and M. Rinard, “Deciding Boolean Algebra with Presburger Arithmetic,” J. Automated Reasoning, accepted for publication, 2006.
[52] D.R. Cheriton and M.E. Wolf, “Extensions for MultiModule Records in Conventional Programming Languages,” Proc. ACM Programming Language Design and Implementation Conf. (PLDI), pp.296306, 1987.
[53] G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. Lopes, J. Loingtier, and J. Irwin, “AspectOriented Programming,” Proc. 15th European Conf. ObjectOriented Programming (ECOOP), June 1997.
[54] V. Kuncak and K.R.M. Leino, “InPlace Refinement for Effect Checking,” Proc. Second Int'l Workshop Automated Verification of InfiniteState Systems (AVIS '03), Apr. 2003.
[55] P. O'Hearn, H. Yang, and J. Reynolds, “Separation and Information Hiding,” Proc. 20th ACM Symp. Principles of Programming Languages (POPL), pp. 268280, 2004.
[56] R. Milner, M. Tofte, R. Harper, and D. MacQueen, The Definition of Standard ML (Revised). MIT Press, 1997.
[57] D.I. Good, R.L. Akers, and L.M. Smith, “Report on Gypsy 2.05,” technical report, Univ. of Texas at Austin, Feb. 1986.
[58] J.R. Abrial, M.K.O. Lee, D. Neilson, P.N. Scharbach, and I. Sørensen, “The BMethod,” Proc. Fourth Int'l Symp. VDM Europe Formal Software Development, vol. 2, pp. 398405, 1991.
[59] C.B. Jones, Systematic Software Development Using VDM. Prentice Hall Int'l Ltd., 1986.
[60] J. Woodcock and J. Davies, Using Z. Prentice Hall, 1996.
[61] J. Guttag and J. Horning, Larch: Languages and Tools for Formal Specification. SpringerVerlag, 1993.
[62] B. Dandanell, “Rigorous Development Using RAISE,” Proc. Conf. Software for Citical Systems, pp. 2943, 1991.
[63] J.C. King, “A Program Verifier,” PhD dissertation, Carnegie Mellon Univ., 1970.
[64] G. Nelson, “Techniques for Program Verification,” technical report, XEROX Palo Alto Research Center, 1981.
[65] J.C. Filliatre, “Verification of NonFunctional Programs Using Interpretations in Type Theory,” J. Functional Programming, vol. 13, no. 4, pp. 709745, 2003.
[66] J.C. Filliatre and C. Marchí, “MultiProver Verification of CPrograms,” Proc. Int'l Conf. Formal Eng. Methods (ICFEM '04), 2004.
[67] C. Marché, C. PaulinMohring, and X. Urbain, “The Krakatoa Tool for Certification of JAVA/JAVACARD Programs Annotated in JML,” J. Logic and Algebraic Programming, 2003.
[68] L. Burdy, Y. Cheon, D. Cok, M.D. Ernst, J. Kiniry, G.T. Leavens, K.R.M. Leino, and E. Poll, “An Overview of JML Tools and Applications,” Technical Report NIIR0309, Computing Science Inst., Univ. of Nijmegen, Mar. 2003.
[69] D.L. Detlefs, K.R.M. Leino, G. Nelson, and J.B. Saxe, “Extended Static Checking,” Technical Report 159, Compaq Systems Research Center, 1998.
[70] D. Detlefs, G. Nelson, and J.B. Saxe, “Simplify: A Theorem Prover for Program Checking,” Technical Report HPL2003148, HewlettPackard Laboratories Palo Alto, 2003.
[71] G. Nelson, “Verifying Reachability Invariants of Linked Structures,” Proc. ACM Symp. Principles of Programming Languages (POPL), 1983.
[72] T. LevAmi, N. Immerman, T. Reps, M. Sagiv, S. Srivastava, and G. Yorsh, “Simulating Reachability Using FirstOrder Logic with Applications to Verification of Linked Data Structures,” Proc. 20th Int'l Conf. Automated Deduction (CADE 20), 2005.
[73] S.K. Lahiri and S. Qadeer, “Verifying Properties of WellFounded Linked Lists,” Proc. ACM Symp. Principles of Programming Languages (POPL '06), 2006.
[74] D.R. Cok, “Reasoning with Specifications Containing Method Calls and Model Fields,” J. Object Technology, vol. 4, no. 8, pp. 77103, Sept.Oct. 2005.
[75] M. Barnett, R. DeLine, M. Fähndrich, K.R.M. Leino, and W. Schulte, “Verification of ObjectOriented Programs with Invariants,” J. Object Technology, vol. 3, no. 6, pp. 2756, 2004.
[76] K.R.M. Leino and P. Müller, “A Verification Methodology for Model Fields,” Proc. European Symp. Programming (ESOP '06), 2006.
[77] T. Ball, S. Lahiri, and M. Musuvathi, “Zap: Automated Theorem Proving for Software Analysis, Technical Report MSRTR2005137, Microsoft Research, 2005.
[78] S. Chaki, S.K. Rajamani, and J. Rehof, “Types as Models: Model Checking MessagePassing Programs,” Proc. 29th ACM SIGPLANSIGACT Principles of Programming Languages (POPL), pp. 4557, 2002.
[79] P. Meunier, R.B. Findler, and M. Felleisen, “Modular SetBased Analysis from Contracts,” Proc. 33rd ACM Principles of Programming Languages (POPL), pp. 218231, Jan. 2006.
[80] B.Y.E. Chang and K.R.M. Leino, “Abstract Interpretation with Alien Expressions and Heap Structures,” Proc. Conf. Verification, Model Checking and Abstract Interpretation (VMCAI' 05), Jan. 2005.