Institute of Information Science, Academia Sinica

In this talk, we study the construction of shape-numeric static analysers, and the combination of several memory abstracitons in a single shape analysis tool. We set up an abstract interpretation framework that allows to reason about simultaneous shape-numeric properties by combining shape and numeric abstractions into a modular, expressive abstract domain. Such a modular structure is highly desirable to make its formalisation, proof and implementation easier to perform and to get correct. Furthermore, we extend this modular abstract domains so as to combine different memory abstractions, for better scalability and greater expressiveness. This framework is implemented in the MemCAD static analyser.