Galois Connections for Recursive Types

Publikation: Bidrag til bog/antologi/rapportBidrag til bog/antologiForskningfagfællebedømt

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
TitelsFrom Lambda Calculus to Cybersecurity Through Program Analysis : Essays Dedicated to Chris Hankin on the Occasion of His Retirement
Antal sider27
ForlagSpringer VS
Publikationsdato2020
Sider105-131
DOI
StatusUdgivet - 2020
NavnLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind12065 LNCS
ISSN0302-9743

ID: 239017417