# Projects

From Matching Logic

## Contents |

## Current

## Project Ideas

### Model Checking

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

### All-Paths Compositional

Can we get compositional reasoning (think rely-guarantee, separation logic) as a methodological approach within the all-paths system? Do we need new axioms?

### Invariant Inference

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.