Logical Abstract Domains and Interpretations
Abstract
We give semantic foundations to abstract domains consisting in first order logic formulae in a theory, as used in verification tools or methods using SMT-solvers or theorem provers. We exhibit conditions for a sound usage of such methods with respect to multi-interpreted semantics and extend their usage to automatic invariant generation by abstract interpretation.
Domains
Programming Languages [cs.PL]
Origin : Files produced by the author(s)
Loading...