Write a Blog >>
Wed 20 Jan 2016 11:20 - 11:45 at Grand Bay North - Track 1: Algorithmic Verification Chair(s): Arie Gurfinkel

We investigate the model checking problem for symbolic-heap separation logic with user-defined inductive predicates, i.e., the problem of checking that a given stack-heap memory state satisfies a given formula in this language, as arises e.g.~in software testing or runtime verification approaches.

First, we show that the problem is decidable; specifically, we present a bottom-up fixed point algorithm that decides the problem and runs in exponential time in the size of the problem instance.

Second, we show that, while model checking for the full language is EXPTIME-complete, the problem becomes NP-complete or PTIME-solvable when we impose natural syntactic restrictions on the schemata defining the inductive predicates. We additionally present NP and PTIME algorithms for these restricted fragments.

Finally, we report on the experimental performance of our procedures on a variety of specifications extracted from programs, exercising multiple combinations of syntactic restrictions.

Wed 20 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10
Track 1: Algorithmic VerificationResearch Papers at Grand Bay North
Chair(s): Arie Gurfinkel Carnegie Mellon University
10:30
25m
Talk
Temporal Verification of Higher-order Functional Programs
Research Papers
Akihiro Murase , Tachio Terauchi JAIST, Naoki Kobayashi University of Tokyo, Ryosuke Sato University of Tokyo, Hiroshi Unno University of Tsukuba
10:55
25m
Talk
Scaling Network Verification using Symmetry and Surgery
Research Papers
Gordon Plotkin , Nikolaj Bjørner Microsoft Research, Nuno P. Lopes Microsoft Research, Andrey Rybalchenko Microsoft Research, George Varghese Microsoft Research
Pre-print
11:20
25m
Talk
Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
Research Papers
11:45
25m
Talk
Reducing Crash Recoverability to Reachability
Research Papers
Eric Koskinen Yale University, Junfeng Yang Columbia University