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

11:00 - 12:30: VMCAI 2019 - Decision Procedures at Sala III
Chair(s): Kedar NamjoshiBell Labs, Nokia
VMCAI-201911:00 - 11:30
Jochen HoenickeUniversität Freiburg, Tanja SchindlerUniversity of Freiburg
VMCAI-201911:30 - 12:00
Xiaokang QiuPurdue University, Yanjun WangPurdue University
File Attached
VMCAI-201912:00 - 12:30
Charlie MurphyPrinceton University, Zachary KincaidPrinceton University
File Attached