Deryaft - Home Page

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.