Interpreting abstract interpretations in membership equational logic.

*(English)*Zbl 1268.68066
van den Brand, Mark (ed.) et al., RULE 2001. Proceedings of the 2nd international workshop on rule-based programming (Satellite Event of PLI 2001), Florence, Italy, September 4, 2001. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 59, No. 4, 271-285 (2001).

Summary: We present a logical framework in which abstract interpretations can be naturally specified and then verified. Our approach is based on membership equational logic which extends equational logics by membership axioms, asserting that a term has a certain sort. We represent an abstract interpretation as a membership equational logic specification, usually as an overloaded order-sorted signature with membership axioms. It turns out that, for any term, its least sort over this specification corresponds to its most concrete abstract value. Maude implements membership equational logic and provides mechanisms to calculate the least sort of a term efficiently. We first show how Maude can be used to get prototyping of abstract interpretations “for free”. Building on the meta-logic facilities of Maude, we further develop a tool that automatically checks an abstract interpretation against a set of user-defined properties. This can be used to select an appropriate abstract interpretation, to characterize the specific loss of information during abstraction, and to compare different abstractions with each other.

For the entire collection see [Zbl 1266.68020].

For the entire collection see [Zbl 1266.68020].

##### MSC:

68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |

03B70 | Logic in computer science |

PDF
BibTeX
XML
Cite

\textit{B. Fischer} and \textit{G. Roşu}, Electron. Notes Theor. Comput. Sci. 59, No. 4, 271--285 (2001; Zbl 1268.68066)

Full Text:
DOI

##### References:

[1] | Bouhoula, Adel; Jouannaud, Jean-Pierre; Meseguer, José, Specification and proof in membership equational logic, Theoretical computer science, 236, 35-132, (2000) · Zbl 0938.68057 |

[2] | Edmund Clarke, M.; Grumberg, Orna; David Long, E., Model checking and abstraction, ACM trans. programming languages and systems, 16, 5, 1512-1542, (September 1994) |

[3] | Manuel Clavel, F. Durán, Steven Eker, Patrick Lincoln, N. Martí-Oliet, José Meseguer, and J. F. Quesada. The Maude system. In P. Narendran and M. Rusinowitch, editors, Proc. 10th Intl. Conf. Rewriting Techniques and Applications, {\bfvolume 1631} of Lect. Notes Comp. Sci., pages 240-243, Trento, Italy, July 1999. Springer. System Description. |

[4] | Manuel Clavel, Francisco J. Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and José F. Quesada. Maude: Specification and Programming in Rewriting Logic, March 1999. Maude System documentation at http://maude.csl.sri.com/papers. · Zbl 1115.68046 |

[5] | Patrick M. Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. 4th ACM Symp. Principles of Programming Languages, pages 238-252, Los Angeles, California, January 1977. ACM Press. · Zbl 1149.68389 |

[6] | Bernd Fischer, Johann Schumann, and Thomas Pressburger. Generating data analysis programs from statistical models (position paper). In Walid Taha, editor, Proc. Intl. Workshop Semantics Applications, and Implementation of Program Generation, {\bfvolume 1924} of Lect. Notes Comp. Sci., pages 212-229, Montreal, Canada, September 2000. Springer. · Zbl 1044.68527 |

[7] | Joseph Goguen. Order sorted algebra. Technical Report 14, UCLA Computer Science Department, 1978. Semantics and Theory of Computation Series. · Zbl 0939.68710 |

[8] | Goguen, Joseph; Meseguer, José, Completeness of many-sorted equational logic, Houston journal of mathematics, 11, 3, 307-334, (1985) · Zbl 0602.08004 |

[9] | Goguen, Joseph; Meseguer, José, Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theoretical computer science, 105, 2, 217-273, (1992) · Zbl 0778.68056 |

[10] | Goguen, Joseph; Winkler, Timothy; Meseguer, José; Futatsugi, Kokichi; Jouannaud, Jean-Pierre, Introducing OBJ, () |

[11] | José Meseguer. Membership algebra as a logical framework for equational specification. In Proceedings, WADT’97, {\bfvolume 1376} of Lecture Notes in Computer Science, pages 18-61. Springer, 1998. · Zbl 0903.08009 |

[12] | David Plaisted, A., Theorem proving with abstraction, Art. intell, 16, 1, 47-108, (1981) · Zbl 0454.68113 |

[13] | Willem Visser, S. Park, and John Penix. Using predicate abstraction to reduce object-oriented programs for model checking. In Proceedings of the 3rd ACM SIGSOFT Workshop on Formal Methods in Software Practice, August 2000. To appear. |

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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.