Open Problems and Challenges

From FSL
Revision as of 11:59, 26 January 2016 by Grosu (Talk | contribs)

Jump to: navigation, search

(back to Grigore Rosu's webpage) (back to the Programming Language Design and Semantics webpage)

Here is a list of open problems and challenges in K and matching logic. While we are doing our best to keep this list actual, it may well be the case that some of the problems have been solved in the meanwhile or that we have found a different way to approach the problem. In case you are interested in working on any of these problems, please send us a note at ( to make sure that the problem is still actual and nobody is already working on it. If you are not part of our team already and would like to be or to collaborate with us, please let us know.

  1. 'Dynamic matching logic.' Currently (Jan 2016), we are framing matching logic as a static logic, that is, as one for reasoning about program configurations at a particular place in the execution of a program:
    Matching Logic --- Extended Abstract 
    Grigore Rosu
    RTA'15, Leibniz International Proceedings in Informatics (LIPIcs) 36, pp 5-21. 2015
    PDF, Slides(PPTX), Matching Logic, DOI, RTA'15, BIB
    For dynamic properties we use reachability logic:
    All-Path Reachability Logic 
    Andrei Stefanescu and Stefan Ciobaca and Radu Mereuta and Brandon Moore and Traian Florin Serbanuta and Grigore Rosu
    RTA'14, LNCS 8560, pp 425-440. 2014
    PDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIB
    One-Path Reachability Logic 
    Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
    LICS'13, IEEE, pp 358-367. 2013
    PDF, Slides(PPTX), Reachability Logic, LICS'13, BIB
    However, both one-path and all-path reachability rules are particular formulae in a more general dynamic matching logic', which extends matching logic with two constructs: a modal next construct and a usual fixed-point mu construct. The resulting logic is expected to be sound and relatively complete; the relativity comes from the fact that we will want to fix a model of configurations, same like in reachability logic, to enable the use of SMT solvers for domain reasoning.
  2. list item A2
Personal tools