Constraint Horn Clauses (CHCs) provide a promising foundation for program verification. They combine first-order logic with background theories (like arithmetic or arrays) and can encode program semantics, invariants, and safety properties in a uniform way. Many state-of-the-art verification tools (e.g., Z3 Spacer, Eldarica, SeaHorn) rely on CHCs as their core representation. Potential areas of focus include:
- Encoding state and invariants of class objects
- Modeling methods, constructors, and destructors as logical transitions
- Handling inheritance and polymorphism in the CHC framework
- Checking safety properties (e.g., memory safety, invariants, assertions) This project offers an opportunity to gain hands-on experience in static analysis tools and CHCs. For further information or to express your interest feel free to reach out.