From Matching Logic
Revision as of 18:14, 23 April 2013 by Bmmoore (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search



Conditional All-Paths

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.

Personal tools