Welcome to Deryaft Home Page
Deryaft is a tool that discovers representation
invariants of structurally complex data manipulated by java programs. By
structurally complex data we mean that the inputs are structural (e.g.,
represented with linked data structures) and must satisfy complex constraints
that relate parts of the structure (e.g., acyclicity for linked data
structures).
Given a small set of concrete structures, Deryaft analyzes
their key characteristics to formulate local and global properties that the
structures exhibit. For effective formulation of structural invariants, Deryaft
focuses on graph properties and views the program heap as an edge-labeled
graph.
The invariants generated by Deryaft directly enable automation of various existing frameworks, such as the Korat test generation framework and the Juzi data structure repair framework, which otherwise require the user to provide the invariants.
