Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 12:00 - 12:30 at Sala III - Decision Procedures Chair(s): Kedar Namjoshi

This paper presents an algorithm for the structure embedding problem: given two finite first-order structures over a common relational vocabulary, does there exist an injective homomorphism from one to the other? The structure embedding problem is NP-complete in the general case, but for monadic structures (each predicate has arity <= 1) we observe that it can be solved in polytime by reduction to bipartite graph matching. Our algorithm, MatchEmbeds, extends the bipartite matching approach to the general case by using it as the foundation of a backtracking search procedure. We show that MatchEmbeds outperforms state-of-the-art SAT, CSP, and subgraph isomorphism solvers on difficult random instances and significantly improves the performance of a client model checker for multi-threaded programs.

A Practical Algorithm for Structure Embedding Slides (vmcai_2019_slides.pdf)5.27MiB

Mon 14 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

11:00 - 12:30: Decision ProceduresVMCAI at Sala III
Chair(s): Kedar NamjoshiBell Labs, Nokia
11:00 - 11:30
Solving and Interpolating Constant Arrays Based on Weak Equivalences
Jochen HoenickeUniversität Freiburg, Tanja SchindlerUniversity of Freiburg
11:30 - 12:00
A Decidable Logic for Tree Data-Structures with Measurements
Xiaokang QiuPurdue University, Yanjun WangPurdue University
File Attached
12:00 - 12:30
A Practical Algorithm for Structure Embedding
Charlie MurphyPrinceton University, Zachary KincaidPrinceton University
File Attached