Horn Clauses

Constrained Horn clauses have emerged recently as an intermediate layer in the process of software verification. Verification tasks from many different domains can be encoded to the common language of constrained Horn clauses (CHC) and a single CHC solver can be re-used for the actual solving. This project aims to develop an efficient and reliable CHC solver to facilitate the development and deployment of verification frameworks.

Check out our CHC solver Golem.

Publications:

  1. SolCMC: Solidity Compiler’s Model Checker , Alt Leonardo, Blicha Martin, Hyvärinen Antti E. J., and Sharygina Natasha , CAV, Haifa, Isreal, (2022)
  2. Split Transition Power Abstraction for Unbounded Safety, Blicha Martin, Fedyukovich Grigory, Hyvärinen Antti E. J., and Sharygina Natasha , (2022)
  3. Transition Power Abstractions for Deep Counterexample DetectionBlicha Martin, Fedyukovich Grigory, Hyvärinen Antti E. J., and Sharygina Natasha , TACAS, (2022)