Galois Connections for Recursive Types

Ahmad Salim Al-Sibahi, Thomas P. Jensen, Rasmus Ejlers Møgelberg, Andrzej Wasowski

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelBidrag til bog/antologiForskningpeer review

Abstract

Building a static analyser for a real language involves modeling of large domains capturing the many available data types. To scale domain design and support efficient development of project-specific analyzers, it is desirable to be able to build, extend, and change abstractions in a systematic and modular fashion. We present a framework for modular design of abstract domains for recursive types and higher-order functions, based on the theory of solving recursive domain equations. We show how to relate computable abstract domains to our framework, and illustrate the potential of the construction by modularizing a monolithic domain for regular tree grammars. A prototype implementation in the dependently typed functional language Agda shows how the theoretical solution can be used in practice to construct static analysers.
OriginalsprogEngelsk
TitelFrom Lambda Calculus to Cybersecurity Through Program Analysis
ForlagSpringer
Publikationsdato2020
Sider105-131
ISBN (Trykt)978-3-030-41102-2
ISBN (Elektronisk)978-3-030-41103-9
DOI
StatusUdgivet - 2020
NavnLecture Notes in Computer Science
Vol/bind12065
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Galois Connections for Recursive Types'. Sammen danner de et unikt fingeraftryk.

Citationsformater