Languages, Verification

The past three decades have seen the creation of several tools that extract, visualize, and manipulate graph-structured representations of program information. To facilitate interconnection and exchange of information between these tools, and to support the prototyping and development of new tools, it is desirable to have some generic support for the specification of graph transformations and exchanges between them. GENSET is a generic programmable tool for transformation of graph-structured data. The implementation of the GENSET system and the programming paradigm of its language are both based on the view of a directed graph as a binary relation. Rather than use traditional relational algebra to specify transformations, however, we opt instead for the more expressive class of flow equations. Flow equations—or, more generally, systems of simultaneous fixpoint equations—have seen fruitful applications in several areas, including data and control flow analysis, formal verification, and logic programming. In GENSET, they provide the fundamental construct for the programmer to use in defining new transformations. Categories and Subject Descriptor