SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.
Citation: | Zhao-Peng Li, Yu Zhang, Yi-Yun Chen. A Shape Graph Logic and A Shape System[J]. Journal of Computer Science and Technology, 2013, 28(6): 1063-1084. DOI: 10.1007/s11390-013-1398-1 |
[1] |
Paulson L C. Isabelle: A Generic Theorem Prover. SpringerVerlag Berlin, 1994.
|
[2] |
Nanevski A, Morrisett G, Shinnar A, Govereau P, Birkedal L. Ynot: Dependent types for imperative programs. In Proc. the 13th ACM SIGPLAN Int. Conf. Functional Programming, September 2008, pp.229-240.
|
[3] |
Barnett M, M. Leino K R, Schulte W. The spec# programming system: An overview. In Proc. Int. Conf. Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS), March 2004, pp.49-69.
|
[4] |
Flanagan C, Rustan K, Lillibridge M et al. Extended static checking for Java. In Proc. the ACM SIGPLAN 2002 Conf. Programming Language Design and Implementation, June 2002, pp.234-245.
|
[5] |
Berdine J, Calcagno C, O'Hearn P W. Smallfoot: Modular automatic assertion checking with separation logic. In Proc. the 4th Int. Symp. Formal Methods for Components and Objects, Nov. 2005, pp.115-137.
|
[6] |
Distefano D, Parkinson M. jStar: Towards practical verification for Java. In Proc. the 23rd ACM SIGPLAN Int. Conf. Object-Oriented Programming, Systems, Languages, and Applications, Oct. 2008, pp.213-226.
|
[7] |
Li Z P, Zhang Y, Chen Y Y, Meng J C. Automated theorem proving for theory of shape graphs and its application in program verification. Technical Report, USTCYale Joint Research Center for High-Confidence Software, http://kyhcs.ustcsz.edu.cn/SGL, Nov. 2012.
|
[8] |
Chen Y Y, Li Z P, Wang Z F, Hua B J. A pointer logic for pointer program verification. Chinese Journal of Software, 2010, 21(3): 124-137. (Chinese, English Version at http://kyhcs.ustcsz.edu.cn/?zpli/pl.pdf)
|
[9] |
Fradet P, Metayer D L. Shape types. In Proc. the ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 1997, pp.27-39.
|
[10] |
de Moura L D, Bjørner N. Z3: An efficient SMT solver. In Proc. the 14th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, Mar. 29-Apr. 6, 2008, pp.337-340.
|
[11] |
Lahiri S, Qadeer S. Verifying properties of well-founded linked lists. In Proc. the 33rd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2006, pp.115126.
|
[12] |
Chin W N, David C, Nguyen H H, Qin S. Automated verification of shape, size and bag properties. In Proc. the 12th Int. Conf. Engineering of Complex Computer Systems, July 2007, pp.307-320.
|
[13] |
Lahiri S, Qadeer S. Back to the future: Revisiting precise program verification using SMT solvers. In Proc. the 35th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2008, pp.171-182.
|
[14] |
Bouajjani A, Dragoi C, Enea C, Sighireanu M. A logic-based framework for reasoning about composite data structures. In Proc. the 20th Int. Conf. Concurrency Theory, Sept. 2009, pp.178-195.
|
[15] |
Madhusudan P, Parlato G, Qiu X K. Decidable logics combining heap structures and data. In Proc. the 38th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2011, pp.611-622.
|
[16] |
Reynolds J C. Separation logic: A logic for shared mutable data structures. In Proc. the 17th IEEE Symp. Logic in Computer Science, July 2002, pp.55-74.
|
[17] |
O'Hearn P W, Yang H, Reynolds J C. Separation and information hiding. In Proc. the 31st ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2004, pp.268-280.
|
[18] |
Pérez J A N, Rybalchenko A. Separation logic + superposition calculus = Heap theorem prover. In Proc. ACM SIGPLAn Conf. Programming Language Design and Implementation, Jun. 2011, pp.556-566.
|
[19] |
Berdine J, Calcagno C, O'Hearn P W. A decidable fragment of separation logic. In Proc. the 24th Int. Conf. Foundations of Software Technology and Theoretical Computer Science, Dec. 2004, pp.97-109.
|
[20] |
Sagiv M, Reps T, Wilhelm R. Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems, 1998, 20(1): 1-50.
|
[21] |
Sagiv M, Reps T, Wilhelm R. Parametric shape analysis via 3valued logic. ACM Transactions on Programming Languages and Systems, 2002, 24(3): 217-298.
|
[22] |
Lee O, Yang H, Yi K. Automatic verification of pointer programs using grammar-based shape analysis. In Proc. the 19th European Conf. Programming Languages and Systems, Apr. 2005, pp.124-140.
|
[23] |
Chang B E, Rival X, Necula G C. Shape analysis with structural invariant checkers. In Proc. the 14th Int. Static Analysis Symp., Aug. 2007, pp.384-401.
|
[24] |
Chang B E, Rival X. Relational inductive shape analysis. In Proc. the 35th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2008, pp.247-260.
|
[25] |
Laviron V, Chang B E, Rival X. Separating shape graphs. In Proc. the 19th European Conf. Programming Languages and Systems, Mar. 2010, pp.387-406.
|
[26] |
Lev-Ami T, Reps T, Sagiv M, Wilhelm R. Putting static analysis to work for verification: A case study. In Proc. the Int. Symp. Software Testing and Analysis, Aug. 2000, pp.26-38.
|
[27] |
Clarke E M, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-guided abstraction refinement. In Proc. the 12th Int. Conf. Computer Aided Verification, July 2000, pp.154-169.
|
[28] |
Podelski A, Wies T. Counterexample-guided focus. In Proc. the 27th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2010, pp.249-260.
|
[29] |
Madhusudan P, Qiu X K, Stefanescu A. Recursive proofs for inductive tree data-structures. In Proc. the 39th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2012, pp.123-135.
|
[30] |
Calcagno C, Distefano D, O'Hearn P W, Yang H. Compositional shape analysis by means of bi-abduction. In Proc. the 36th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2009, pp.289-300.
|
[1] | Yong-Liang Yang, Chao-Hui Shen. Multi-Scale Salient Features for Analyzing 3D Shapes[J]. Journal of Computer Science and Technology, 2012, 27(6): 1092-1099. DOI: 10.1007/s11390-012-1287-z |
[2] | NIE Xumin, GUO Qing. Renaming a Set of Non-Horn Clauses[J]. Journal of Computer Science and Technology, 2000, 15(5): 409-415. |
[3] | YANG Lu. Recent Advances in Automated Theorem Proving on Inequalities[J]. Journal of Computer Science and Technology, 1999, 14(5): 434-446. |
[4] | LIN Hua, LU Mi, Jesse Z.FANG. A Direct Approach for Finding Loop Transformation Matrices[J]. Journal of Computer Science and Technology, 1996, 11(3): 237-256. |
[5] | Zhao Zhaokeng, Dai Jun, Chen Wendan. Automated Theorem Proving in Temporal Logic:T-Resolution[J]. Journal of Computer Science and Technology, 1994, 9(1): 53-62. |
[6] | Xue Jinyun. Two New Strategies for Developing Loop Invariants and Their Applications[J]. Journal of Computer Science and Technology, 1993, 8(2): 51-58. |
[7] | Wang Zhijian. Validating Inductive Hypotheses by Mode Inference[J]. Journal of Computer Science and Technology, 1993, 8(2): 37-41. |
[8] | Shen Xubang, Ma Guangti, Chen Lan. An Inference Microprocessor Design[J]. Journal of Computer Science and Technology, 1991, 6(3): 209-213. |
[9] | Jiang Xinjie, Xu Yongsen. A Proof Rule for While Loop in VDM[J]. Journal of Computer Science and Technology, 1989, 4(2): 178-183. |
[10] | Li Layuan. A Routing Algorithm for Distributed Optimal Double Loop Computer Networks[J]. Journal of Computer Science and Technology, 1987, 2(2): 92-98. |