about this paper

presentation abstract bibitem

downloads

slides paper editor link
Marc Chevalier and Jérôme Feret.
Sharing ghost variables in a collection of abstract domains.
In Proceedings of the Twenty-First International Conference on Verification, Model Checking and Abstract Interpretation, VMCAI'20. New Orleans, USA, D. Beyer and D. Zufferay (Eds), Lecture Notes in Computer Science 11990, pp 158--179.
© Springer, Berlin, Germany.

Abstract: We propose a framework in which we share ghost variables across a collection of abstract domains allowing precise proofs of complex properties.
In abstract interpretation, it is often necessary to be able to express com- plex properties while doing a precise analysis. A way to achieve that is to combine a collection of domains, each handling some kind of properties, using a reduced product. Separating domains allows an easier and more modular implementation, and eases soundness and termination proofs. This way, we can add a domain for any kind of property that is inter- esting. The reduced product, or an approximation of it, is in charge of refining abstract states, making the analysis precise. In program verification, ghost variables can be used to ease proofs of properties by storing intermediate values that do not appear directly in the execution.
We propose a reduced product of abstract domains that allows domains to use ghost variables to ease the representation of their internal state. Domains must be totally agnostic with respect to other existing domains. In particular the handling of ghost variables must be entirely decentral- ized while still ensuring soundness and termination of the analysis. 

@inProceedings{ChevalierEtAl-VMCAI20,
   author =    {Marc Chevalier and J\'er\^ome Feret},
   title =     {Sharing ghost variables in a collection of abstract domains},
   editor =    {Dirk Bayer and Damien Zufferey},
   booktitle = {Proceedings of the Twenty-First International Conference on Verification, Model Checking and Abstract Interpretation, VMCAI$\,$'2020},
   address =   {New Orleans, USA},
   series =    {Lecture Notes in Computer Science},
   volume =    {11990},
   publisher = {Springer, Berlin, Germany},
   pages =     {158--179},
   month =     {19--21 January},
   year =      {2020},
}