Difference between revisions of "Open Problems and Challenges"

Revision as of 13:44, 27 January 2016

(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, in no particular order. 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 (grosu@illinois.edu) 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. Once defined, then we should be able to prove the reachability logic proof system rules as theorems, thus modulo

   From Hoare Logic to Matching Logic Reachability 

   Grigore Rosu and Andrei Stefanescu
   FM'12, LNCS 7436, pp 387-402. 2012
   PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, FM'12, BIB

   obtaining that dynamic matching logic generalizes Hoare logic mechanically. We should also be able to prove that dynamic matching logic similarly generalizes dynamic logic. The point of these generalizations is that Hoare or dynamic logic are basically "design patterns" to be manually crafted for each language separately, while dynamic matching logic is one fixed logic for all languages; each language is a particular set of axioms, which can be used in combination with a language-independent fixed proof system to derive any dynamic property for the language. In our view, that is how program reasoning/verification should be done, using one language-independent and powerful logic, and not to craft a specific logic for each specific language (which is what Hoare/dynamic/separation logic advocate).
2. Coinductive program verification.
3. Formal Relationship between the Circularity proof rule and Coinduction.
4. True concurrency with K.
5. Rewrite-based parsing.
6. Fast execution engine for K.
7. Semantics-based compilation.
8. Semantics-based test-case generation.
9. Language-independent symbolic execution framework.
10. Language-independent infrastructure for program equivalence.
11. Strategy language.
12. Systematic comparison of K with other operational approaches. K evolved from other approaches, systematically analyzing their advantages and disadvantages, and keeping the advantages and eliminating the disadvantages. This is partly explained in my book draft, but it needs to be also published as a conference/journal paper, for wider dissemination. Indeed, we have encountered many scientists who seem to think that K is some new theoretical development based on new principles. Well, sorry to disappoint, but K is an engineering endeavor attempting to get the best of the ideas developed by the formal semantics community over the last four decades, avoiding their limitations. The main novelties of K, besides its unique notation, are: (1) its concurrent semantics, which allows for true concurrency even in the presence of sharing; and (2) its configuration abstraction mechanism which is the key for more modular language definitions.
13. Configuration abstraction.
14. Defining/Implementing language translators/compilers in K. Either in translation-validation style or provably correct.