search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
200 stars 41 forks source link

iCfg to CHC translation #421

Closed alexandernutz closed 1 week ago

alexandernutz commented 5 years ago

Implement a plugin that translates from an icfg/rcfg to a set of constrained Horn clauses (CHCs) such that the CHC-set is satisfiable iff the icfg is correct/safe.

danieldietsch commented 5 years ago

@alexandernutz can this issue be closed?

schuessf commented 1 week ago

There is a plugin Library-CHC with this functionality.