Anzeige
Erschienen in:
2006 | OriginalPaper | Buchkapitel
Separation Logic and Program Analysis
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Separation logic is a program logic for reasoning about programs that manipulate pointer data structures. It has a strong form of modularity or locality built in, and has led to simpler by-hand proofs of pointer algorithms than was possible in previous formalisms. It is natural to wonder whether, and in what way, its ideas might be used in program analysis.
In this talk I will begin by describing the basics of separation logic, along the way connecting them to concepts from program analysis. I will then describe some initial, unsuccessful attempts at applying the formalism. This is done in an effort to convey that some of the first ideas at application do not work well, and also to help pin down what some of the central outstanding issues are. This will then lead on to, and partially justify, one way of organizing a program analysis, where the abstract domain is built from formulae in separation logic. Finally, I will survey some recent developments and speculate on further possibilities.