Abstract interpretation

[Google Scholar] [Wikipedia]

todo:

Boogie: A modular reusable verifier for object-oriented programs [barnett:fmco:2005]
Beyond reachability: Shape abstraction in the presence of pointer arithmetic [calcagno:sas:2006]
Model checking: Algorithmic verification and debugging [clarke:cacm:2009]
An abstract interpretation framework for refactoring with application to extract methods with contracts [cousot:oopsla:2012]
Frama-C: A software analysis perspective [cuoq:sefm:2012]
A local shape analysis based on separation logic [distefano:tacas:2006]
Static contract checking with abstract interpretation [fahndrich:foveoos:2010]
The SeaHorn verification framework [gurfinkel:cav:2015]
Absynthe: Abstract interpretation-guided synthesis [guria:pldi:2023]
TSL: A system for generating abstract interpreters and its application to machine-code analysis [lim:toplas:2013]
Verifying security invariants in ExpressOS [mai:asplos:2013]
Dataflow-based pruning for speeding up superoptimization [mukherjee:oopsla:2020]
HOIST: a system for automatically deriving static analyzers for embedded systems [regehr:asplos:2004]
Eliminating stack overflow by abstract interpretation [regehr:emsoft:2003]
Deriving abstract transfer functions for analyzing embedded software [regehr:lctes:2006]
Eliminating stack overflow by abstract interpretation [regehr:tecs:2005]

Notes related to Abstract interpretation