Abstract | ||
---|---|---|
We introduce a notion of subsumption for domains used in abstract interpretation. We show that subsumption has the same properties and applications in the context of abstract interpretation that simulation has for transition systems. These include a modal characterisation theorem, a fixed point characterisation, and the construction of property-preserving abstractions. We use the notion of conjugate functions from algebraic logic to develop bisubsumption, an order-theoretic generalisation of bisimulation to Boolean domains. We prove a representation theorem that relates simulation and subsumption. |
Year | DOI | Venue |
---|---|---|
2013 | 10.1007/978-3-642-40184-8_34 | CONCUR |
Keywords | Field | DocType |
fixed point characterisation,abstract domain,generalizing simulation,modal characterisation theorem,abstract interpretation,order-theoretic generalisation,transition system,conjugate function,boolean domain,algebraic logic,representation theorem,property-preserving abstraction | Transition system,Discrete mathematics,Abstract interpretation,Computer science,Representation theorem,Algebraic logic,Theoretical computer science,Modal logic,Bisimulation,Complete lattice,Fixed point | Conference |
Citations | PageRank | References |
1 | 0.35 | 19 |
Authors | ||
1 |
Name | Order | Citations | PageRank |
---|---|---|---|
Vijay D'Silva | 1 | 239 | 14.07 |