Completeness in static analysis by abstract interpretation, a personal point of view

David Monniaux (1)

1 VERIMAG - IMAG - VERIMAG

Static analysis by abstract interpretation is generally designed to be "sound", that is, it should not claim to establish properties that do not hold-in other words, not provide "false negatives" about possible bugs. A rarer requirement is that it should be "complete", meaning that it should be able to infer certain properties if they hold. This paper describes a number of practical issues and questions related to completeness that I have come across over the years.

Domaines: Langage de programmation [cs.PL]

David Monniaux. Completeness in static analysis by abstract interpretation, a personal point of view. Vincenzo Arceri; Agostino Cortesi; Pietro Ferrara; Martina Olliaro. Challenges of Software Verification, Springer Singapore, 2023, 978-981-19-9600-9. ⟨hal-03857312v1⟩