I remember Frama-C for its slicing. I have recently become interested in Datalog driven approaches, such as Souffle, for static analysis of large codebases. Anyone with experience or thoughts along those lines?
Out of curiosity, are there known pros and cons to each approach? I’ve been experimenting with Z3’s CHC engine and Coq for modeling programs. I don’t know enough about both yet to fully understand how they compare.
