Cited By
View all- Strecker M(2008)Modeling and Verifying Graph Transformations in Proof AssistantsElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2008.03.039203:1(135-148)Online publication date: 1-Mar-2008
Description Logics for Shape Analysis
Pages 321 - 331
Abstract
Verification of programs requires reasoning about sets of program states. In case of programs manipulating pointers, program states are pointer graphs. Verification of such programs involves reasoning about unbounded sets of graphs. Three-valued shape analysis (Sagiv et. al.) is an approach based on explicit manipulation of 3-valued shape graphs, which abstract sets of pointer graphs. Other approaches use symbolic representations, e. g., by describing (sets of) graphs as logical formulas. Unfortunately, many resulting logics are either undecidable or cannot express crucial properties like reachability and separation. In this paper, we investigate an alternative approach. We study well-known description logics as a framework for symbolic shape analysis. We propose a predicate abstraction based shape analysis, parameterized by description logics to represent the abstraction predicates. Depending on the particular logic chosen sharing, reachability and separation in pointer data structures are expressible.
References
[1]
F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel-Schneider, editors. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, 2003.
[2]
T. Ball, A. Podelski, and S. Rajamani. Boolean and cartesian abstraction for model checking C programs. In Proc. TACAS'O1, LNCS 2031, pages 268-283. Springer, 2001.
[3]
P. Bonatti and A. Peron. On the undecidability of logics with converse, nominals, recursion and counting. Artificial Intelligence, 158:75-96, 2004.
[4]
D. Calvanese, G. De Giacomo, and M. Lenzerini. Reasoning in expressive description logics with fixpoints based on automata on infinite trees. In Proc. IJCAI'99, pages 84-89. Morgan Kaufmann, 1999.
[5]
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis by construction of approximation of fixed points. In Proc. POPL'77, pages 238-252. ACM Press, 1977.
[6]
P. Fradet and D. Metayer. Shape types. In Proc. POPL'97, pages 27-39. ACM Press, 1997.
[7]
E. Grädel. On the restraining power of guards. J. Symbolic Logic, 64:1719-1742, 1999.
[8]
E. Grädel and I. Walukiewicz. Guarded fixed point logic. In Proc. LICS'99, pages 45-54. IEEE Computer Society Press, 1999.
[9]
S. Graf and H. Saidi. Construction of abstract shape graphs with PVS. In Proc. CAV'97, LNCS 1254, pages 72-83. Springer, 1997.
[10]
V. Haarslev and R. Möller. RACER system description. In Proc. IJCAR'O1, LNCS 2083, pages 29-44. Springer, 2001.
[11]
J. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Proc. TACAS'95, LNCS 1019, pages 89-110, 1995.
[12]
I. Horrocks. Using an expressive description logic: FaCT or fiction? In Proc. KR'98, pages 636-647. Morgan Kaufman, 1998.
[13]
N. Immerman, A. Rabinovich, T. Reps, M. Sagiv, and G. Yorsh. The boundary between decidability and undecidability for transitive-closure logics. In Proc. CSL'04, LNCS 3210, pages 160-174. Springer, 2004.
[14]
N. Immerman, A. Rabinovich, T. Reps, M. Sagiv, and G. Yorsh. Verification via structure simulation. In Proc. CAV'04, LNCS 3114, pages 281-294. Springer, 2004.
[15]
D. Kozen. Results on the propositional µ-calculus. In Proc. ICALP'82, LNCS 140, pages 348-359. Springer, 1982.
[16]
V. Kuncak and M. Rinard. On role logic. Technical Report 925, MIT Computer Science and Artificial Intelligence Laboratory, 2003.
[17]
T. Lev-Ami and S. Sagiv. TVLA: A system for implementing static analyses. In Proc. SAS'00, LNCS 1824, pages 280-301. Springer, 2000.
[18]
A. Møller and M. I. Schwartzbach. The pointer assertion logic engine. In Proc. PLDI'O1, pages 221-231, 2001.
[19]
A. Podelski and T. Wies. Boolean heaps. In Proc. SAS'05, 2005. To appear.
[20]
I. Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers. J. of Logic, Language and Information. To appear.
[21]
A. Rensink. Canonical graph shapes. In Proc. ESOP'04, LNCS 2986, pages 401-415. Springer, 2004.
[22]
M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. TOPLAS, 24:217-298, 2002.
[23]
U. Sattler and M. Y. Vardi. The hybrid µ-calculus, In Proc. IJCAR'01, LNAI 2083, pages 76-91. Springer, 2001.
[24]
M. Schmidt-Schauß and G. Smolka. Attributive concept descriptions with complements. J. Artificial Intelligence, 48: 1- 26, 1991.
[25]
R. S. Streett and E. A. Emerson. An automata theoretic decision procedure for the propositional µ-calculus. Information and Computation, 81:249-264, 1989.
[26]
C. Weidenbach, U. Brahm, T. Hillenbrand, E. Keen, C. Theobald, and D. Topic. SPASS version 2.0. In Proc. CADE'02, LNCS 2392, pages 275-279. Springer, 2002.
[27]
T. Wies. Symbolic shape analysis. Master's thesis, MPI Informatik, Saarbrücken, Germany, 2004.
[28]
G. Yorsh, T. Reps, and S. Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In Proc. TACAS'04, LNCS 2988, pages 530-545. Springer, 2004.
Index Terms
- Description Logics for Shape Analysis
Recommendations
Intuitionistic Trilattice Logics
We take up a suggestion by Odintsov (2009, Studia Logica, 91, 407–428) and define intuitionistic variants of certain logics arising from the trilattice SIXTEEN3 introduced in Shramko and Wansing (2005, Journal of Philosophical Logic, 34, 121–153 and ...
Constructive Description Logics Hybrid-Style
Constructive modal logics come in several different flavours and constructive description logics, not surprisingly, do the same. We introduce an intuitionistic description logic, which we call iALC (for intuitionistic ALC, since ALC is the name of the ...
Model comparison games for horn description logics
LICS '19: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer ScienceHorn description logics are syntactically defined fragments of standard description logics that fall within the Horn fragment of first-order logic and for which ontology-mediated query answering is in PTime for data complexity. They were independently ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2005
433 pages
ISBN:0769524354
Publisher
IEEE Computer Society
United States
Publication History
Published: 07 September 2005
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 17 Dec 2024
Other Metrics
Citations
Cited By
View all- Strecker M(2008)Modeling and Verifying Graph Transformations in Proof AssistantsElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2008.03.039203:1(135-148)Online publication date: 1-Mar-2008