Open Problems and Challenges
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 (firstname.lastname@example.org) 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.
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
- 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
- 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
- Unifying deductive program verification and model checking. It is already there, only needs to be written up.
- Coinductive program verification.
- Formal Relationship between the Circularity proof rule and Coinduction.
- True concurrency with K.
- Rewrite-based parsing.
- Fast execution engine.
- Semantics-based compilation.
- Support full dynamic matching logic in K.
- Semantics-based test-case generation.
- Symbolic execution framework.
- Symbolic model checking.
- Aggressive state/configuration-reduction techniques. Graph-isomorphism, alpha-equivalence, user-defined abstractions.
- Language-independent infrastructure for program equivalence.
- C program portability checking.
- Verifying compiler optimizations and even complete compiler. LLVM.
- Strategy language.
- 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.
- Configuration abstraction.
- Defining/Implementing language translators/compilers in K. Translation-validation style, or provably correct style, or both.
- Translations from K to other languages or formalisms. Maude, OCAML, Coq, Haskell, LLVM, etc. Both interpreters and compilers.
- Coq certification of proofs using K framework.
- Matching logic proof checker/certifier.
- Novel verification methodologies. Our verification approach opens the door for novel verification methodologies. Aspects, runtime verification.
- Reachability logic proof system with conditional rules (the challenge is the all-path).
So going through Coq is unnecessary.