Property Generation

Goal - Automated Property Generation for smart contracts.

1. Invariant Generation
2. Automated Test Generation
3. Formal Specs Generation

Invariant Generation

Currently we follow templates based structure for invariants. We supprt ERC20 tokens. Adding more templates as we go. Developers can use this template as a cookie cutter, change the values to fit their need and then we generate invariants for them. Based on - Slither Property Generation

Automated Test Generation

Using DynaMOSA algorithm to traverse the CGF and generate viable test cases for functions allowing high code coverage.

Formal Specs Generation

This too will be template based for now. Just like Invariant generation