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

We present a new solver and interpolation algorithm for the theory of arrays with constant arrays. It is based on our previous work on weakly equivalent arrays. Constant arrays store the same value at every index, which is useful for model checking of programs with initialised memory. Instead of using a store chain to explicitly initialise the memory, using a constant array can considerably simplify the queries and thus reduce the solving and interpolation time. We show that only a few new rules are required for constant arrays and prove the correctness of the decision procedure and the interpolation procedure. We implemented the algorithm in our interpolating solver SMTInterpol.

Mon 14 Jan

Displayed time zone: Belfast change

11:00 - 12:30
Decision ProceduresVMCAI at Sala III
Chair(s): Kedar Namjoshi Bell Labs, Nokia
11:00
30m
Talk
Solving and Interpolating Constant Arrays Based on Weak Equivalences
VMCAI
Jochen Hoenicke Universität Freiburg, Tanja Schindler University of Freiburg
11:30
30m
Talk
A Decidable Logic for Tree Data-Structures with Measurements
VMCAI
Xiaokang Qiu Purdue University, Yanjun Wang Purdue University
File Attached
12:00
30m
Talk
A Practical Algorithm for Structure Embedding
VMCAI
Charlie Murphy Princeton University, Zachary Kincaid Princeton University
File Attached