Make a principled model checker based on the all-paths matching logic system
Symbolic All-Paths Execution
Related to model checking, use the symbolic execution engine to explore nondeterministic languages
Can we get compositional reasoning (think rely-guarantee, separation logic) as a methodological approach within the all-paths system? Do we need new axioms?
Try to infer program invariants from executions in K. Think of Daikon, with a bit more anti-unification.
Decidable fragments of Logic
Look at the decidable heap logics like Strand, Dryad that Andrei has worked on with Madhu, and see if we can integrate them as abstract heap patterns in a matching logic.