Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
Tue 17 Jan 2017 14:00 - 14:30 at Amphitheater 44 - Abstract Interpretation Chair(s): Roberto Giacobazzi

In abstract interpretation, the notion of forward-completeness with respect to a logic guarantees that an abstract and a concrete structure satisfy exactly the same formulae. We apply completeness to study models of positive modal logic, which are logics that lack negation and implication. These models, which were discovered independently by re- searchers in abstract interpretation, modal logic and model checking, are Kripke structures with an order on states and their lattice-theoretic duals. We show that forward-complete abstractions are models of certain modal logics. The Kripke structures corresponding to these models satisfy a saturation condition ensuring that modal operators have the same properties as best abstract transformers. We synthesize a new notion of simulation for these models using the constructive characterization of complete abstractions.

Tue 17 Jan

VMCAI-2017-papers
14:00 - 15:30: VMCAI - Abstract Interpretation at Amphitheater 44
Chair(s): Roberto GiacobazziUniversity of Verona, Italy
VMCAI-2017-papers14:00 - 14:30
Talk
Vijay D'SilvaGoogle, Marcelo SousaUniversity of Oxford
VMCAI-2017-papers14:30 - 15:00
Talk
David B├╝hlerCEA LIST, Boris YakobowskiCEA - LIST, Sandrine BlazyUniversity of Rennes 1, France
Media Attached
VMCAI-2017-papers15:00 - 15:30
Talk
Mooly SagivTel Aviv University, Or OzeriTel Aviv university, Oded PadonTel Aviv University, Noam RinetzkyTel Aviv University
Media Attached