Difference between revisions of "Open Problems and Challenges"

From FSL
Jump to: navigation, search
Line 61: Line 61:
 
This would be a fundamental result in the field, helping future generations of designers and developers of programming languages and program verification tools to do all these better: define a formal operational semantics of your language in any formalism you like, and that's all, because the desired program verification logic for your language comes for free and it is not only sound, but also relatively complete.
 
This would be a fundamental result in the field, helping future generations of designers and developers of programming languages and program verification tools to do all these better: define a formal operational semantics of your language in any formalism you like, and that's all, because the desired program verification logic for your language comes for free and it is not only sound, but also relatively complete.
 
For all practical reasons we already have that in K, thanks to the last paper above, but the challenge for the perfect result remains.
 
For all practical reasons we already have that in K, thanks to the last paper above, but the challenge for the perfect result remains.
 +
 +
adnsdfs
 +
fsddsd
 +
 +
sdsdf
 +
gsgfs
 +
 +
sdgf
 +
sdfg
 +
 
</li>
 
</li>
  

Revision as of 13:16, 30 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, 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. Sound and relatively complete reachability logic proof system with conditional rules (the challenge is the all-path).
  3. The original reachability logic proof systems that we proposed and proved sound and relatively complete, namely

    Towards a Unified Theory of Operational and Axiomatic Semantics 
    Grigore Rosu and Andrei Stefanescu
    ICALP'12, LNCS 7392, pp 351-363. 2012
    PDF, Slides(pptx), Slides(pdf), Matching Logic, ICALP'12, 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, FM'12, , BIB

    Checking Reachability using Matching Logic 
    Grigore Rosu and Andrei Stefanescu
    OOPSLA'12, ACM, pp 555-574. 2012
    PDF, Slides(pptx), Slides(pdf), Matching Logic, OOPSLA'12, BIB

    worked only with language semantics defined using unconditional reachability rules and deriving one-path reachability rules. These are sufficient for deterministic language semantics in several frameworks, including in K. We tried hard to eliminate the "unconditional" and the "one-path" limitations, but we only partially succeeded.

    First, we were able to extend our soundness and relative completeness results to allow semantics defined using conditional rules, but still deriving only one-path reachability rules:

    Reachability Logic 
    Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca and Brandon Moore
    Technical Report http://hdl.handle.net/2142/32952, July 2012
    PDF, TR@UIUC

    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

    Now thanks to this paper,

    A Rewriting Logic Approach to Operational Semantics 
    Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer
    Information and Computation, Volume 207(2), pp 305-340. 2009
    PDF, Experiments, J.Inf.&Comp., BIB

    which shows that virtually all operational semantics approaches can be represented using rewriting with conditional rules, at least we have a general language-independent (sound and relatively complete) verification infrastructure that works with any deterministic language defined using any operational semantic formalism. We say "deterministic language" above, because for non-deterministic languages we typically want to prove all-path reachability.

    Second, we were able to extend our results to prove all-path reachability, but only when the language semantics is defined using unconditional rules:

    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

    This is good enough for us in K, because the language semantics that we define in K consist of unconditional reachability rules, so we stopped here with our quest.

    However, scientifically speaking, it is very frustrating that we were not able to find a perfect solution to such a beautiful and major problem! It should be possible to obtain a sound and relatively complete proof system for a combined logic with both one-path and all-path conditional reachability rule statements, where the target programming language semantics is nothing but a subset of such rules. Such a proof system would completely eliminate the need for Hoare logic or axiomatic semantics or any other semantics used for program verification, and all the heavy work on proving such semantics sound and relatively complete with respect to a reference model operational semantics of the language, simply because the proof system itself gives you that, for any language, be it concurrent or not, defined using any operational semantic style. This would be a fundamental result in the field, helping future generations of designers and developers of programming languages and program verification tools to do all these better: define a formal operational semantics of your language in any formalism you like, and that's all, because the desired program verification logic for your language comes for free and it is not only sound, but also relatively complete. For all practical reasons we already have that in K, thanks to the last paper above, but the challenge for the perfect result remains.

    adnsdfs fsddsd

    sdsdf gsgfs

    sdgf sdfg


  4. Unifying deductive program verification and (symbolic) model checking. adnsdfs fsddsd sdsdf gsgfs sdgf sdfg In our approach, there is no distinction between deductive verification and model checking. These are just particular uses of our fixed and language-independent proof system, to derive particular properties about particular languages. Moreover, optimizations made for one can apply to the other. For example, a faster matching logic prover will give us faster deductive reasoning and also faster model checking. Also, a faster checker for already visited configurations/states (better hashing), will obviously give us a faster model checker, but it will also give us faster verifier because the circularity rule will be applied more effectively. I can personally think of no difference between a "model checker" and a "deductive program verifier" in our approach. But this needs to be spelled out rigorously and empirically. We should implement automated proof search optimizations that give users the feel of a "model checker", at the same time having the system generate a proof object using our proof system, as a checkable proof certificate of what the model checker did. Much of the research in the model checking field goes into developing alogorithms, such as automata-based ones, where the automata encode both the program and the property to check. This approach is particularly useful for explicit-state model checking, but not only. Then there is also much work on using BDDs for symbolic model checking. We should also consider such algorithms, but then we should still be able to generate a proof object as a result of the analysis. My conjecture is the following. The key ingredient that makes our approach particularly suitable for such a grande unification is the Circularity rule. See for example this paper, but any of the papers mentioned under the "dynamic matching logic" challenge works:
    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
    Check the Circularity proof rule out. It is saying that if you want to prove a reachability property, then assume it and try to prove it, but use it in your proof only after you make one trusted step with the operational semantic rules. This is very similar to how model checkers saturate their state-space search. We should be able to take model checking algorithms and adapt them to work with the general-purpose transition systems that semantics associate to programs, and then take their verification results and translate them into proofs using our proof system, where cycles in the internal graphs or automata maintained by the model checker result in applications of the Circularity rule.

  5. Coinductive program verification. adnsdfs fsddsd sdsdf gsgfs sdgf sdfg





  6. Formal Relationship between the Circularity proof rule and Coinduction.
  7. True concurrency with K.
  8. Rewrite-based parsing.
  9. Fast execution engine.
  10. Semantics-based compilation.
  11. Support full dynamic matching logic in K.
  12. Semantics-based test-case generation.
  13. Symbolic execution framework.
  14. Symbolic model checking.
  15. Aggressive state/configuration-reduction techniques. Graph-isomorphism, alpha-equivalence, user-defined abstractions.
  16. Language-independent infrastructure for program equivalence.
  17. C program portability checking.
  18. Verifying compiler optimizations and even complete compiler. LLVM.
  19. Strategy language.
  20. 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.
  21. Configuration abstraction.
  22. Defining/Implementing language translators/compilers in K. Translation-validation style, or provably correct style, or both.
  23. Translations from K to other languages or formalisms. Maude, OCAML, Coq, Haskell, LLVM, etc. Both interpreters and compilers.
  24. Coq certification of proofs using K framework.
  25. Matching logic proof checker/certifier.
  26. So going through Coq is unnecessary.

  27. Novel verification methodologies. Our verification approach opens the door for novel verification methodologies. Aspects, runtime verification.
  28. K semantics to new real languages. Dwight's Python semantics needs to be published. Java 8. JavaScript ES6. SML, OCAML, Haskell, Ruby, C#, Go, etc.

Personal tools
Namespaces

Variants
Actions
Navigation