Horn clauses

[Google Scholar]

Notes:
Papers:

Executable counterexamples in software model checking [gennari:vstte:2018]
The SeaHorn verification framework [gurfinkel:cav:2015]
Beyond the elementary representations of program invariants over algebraic data types [kostyukov:pldi:2021]
RustHorn: CHC-based verification for Rust programs [matsushita:esop:2020]
Simple verification of Rust programs via functional purification [ullrich:msc:2016]

The opinions expressed are my own views and not my employer’s.