Difference between revisions of "Open Problems and Challenges"
Line 93:  Line 93:  
<li>  <li>  
'''Coinductive program verification.'''  '''Coinductive program verification.'''  
−  +  Recall that conventional Hoarestyle program verification typically proves ''partial correctness'' of programs, that is, that a program satisfies its property if it terminates.  
+  The nonterminating programs satisfy any property under partial correctness; in particular, a nonterminating program satisfies the property ''false''.  
+  Partial correctness should not be confused with ''total correctness'', which means that the program terminates and it satisfies the desired property.  
+  Termination is typically handled using different mechanisms (e.g., ''variants'').  
+  Sometimes researchers craft Hoare logics for total correctness, but those tend to be rather intricate.  
+  Now, when partial correctness is sought to be proved, a very nice way to do it is by ''coinduction'':  
<pubbib id='moorerosu2015tr' />  <pubbib id='moorerosu2015tr' />  
+  The main idea is that the partial correctness properties of a programming language are precisely the coinductive closure of the step relation given by the operational semantics of the programming language.  
+  This is not only an interesting theoretical observation, but we believe it can be quite practical.  
+  It shares the same belief of an ideal language framework, where the operational semantics is taken as input and tools are generated from it.  
+  The tool in this case is more of a workbench, where one can use an interactive theorem prover like Coq or Isabelle with support for coinduction, and then do proofs about programs there based only on the existing generic mathematical infrastructure and the operational semantics of the programming language defined as a binary (step) relation.  
+  
+  The main challenge here is to make coinductive program verification practical.  
+  That means developing proof strategies that automate the process.  
+  Most likely those will be quite similar to those in the matching logic prover of K; for example "execute symbolic configuration using operational semantics rules, doing case analysis when multiple rules match, and giving priority to claimed circularities (which in this case would be coinductive hypotheses)".  
+  
+  Achieving the above in a satisfactory manner would be quite exciting news for the mechanical verification community.  
+  Unfortunately, the stateoftheart in mechanical verification (Jan 2016) is to formalize two different semantics of the target programming language, and to prove a special relationship between them.  
+  One semantics is executable (operational or denotational) and serves as a reference model for the language, because it allows you to run programs and see what they do.  
+  The other semantics is axiomatic, essentially a Hoare logic or a verification condition generator based on a hypothetical Hoare logic, and serves for program verification.  
+  The axiomatic semantics tends to be quite involved, so in order to increase confidence in the results of verification, a proof of soundness for the axiomatic semantics wrt the executable semantics is also provided.  
+  In our view and experience, defining even ''one'' formal semantics to a real language (say C or Java) is a huge effort already.  
+  Defining two semantics and proving the soundness theorem is just too uneconomical if it can be avoided.  
+  And it can!  
+  The secret is ''coinduction''.  
+  Indeed, coinduction with the operational semantics of the language gives you a sound and relatively complete verification infrastructure for any language.  
+  And with the right degree of automation, it can be even more practical than the current axiomatic semantics based approached.  
+  Why? Because you are actually ''executing your program all the time'', so whenever the proof gets stuck or is wrong, which is what happens in most of the situations (you really only prove the program once, all the other attempts until you get there are typically wrong steps or stuck proofs), you know exactly where it happened and why.  
+  There is a disadvantage of the coinductive approach, though.  
+  There will be fewer PhD theses on formal semantics of programming languages.  
+  With the current stateoftheart, defining an executable semantics of C is one PhD thesis, defining an axiomatic semantics of C is yet another PhD thesis, and then proving the soundness of the latter semantics in terms of the former semantics is yet another PhD thesis.  
+  This last one will have the merit that it will also fix bugs in the axiomatic semantics, because it will be full of bugs as it is not executable and thus not testable.  
+  And then all the above will be maintained as C evolves (C99 > C11 > ?).  
+  Excuse our sarcasm, but the current stateoftheart is simply unacceptable.  
+  Period.  
</li>  </li>  
Revision as of 22:14, 29 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.

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 521. 2015
PDF, Slides(PPTX), Matching Logic, DOI, RTA'15, BIB
 AllPath 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 425440. 2014
PDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIB
 OnePath Reachability Logic
 Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
LICS'13, IEEE, pp 358367. 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 387402. 2012
PDF, Slides(pptx), Slides(pdf), Matching Logic, FM'12, , BIB
 Sound and relatively complete reachability logic proof system with conditional rules (the challenge is the allpath).
 Towards a Unified Theory of Operational and Axiomatic Semantics
 Grigore Rosu and Andrei Stefanescu
ICALP'12, LNCS 7392, pp 351363. 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 387402. 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 555574. 2012
PDF, Slides(pptx), Slides(pdf), Matching Logic, OOPSLA'12, BIB  Reachability Logic
 Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca and Brandon Moore
Technical Report http://hdl.handle.net/2142/32952, July 2012
PDF, TR@UIUC  OnePath Reachability Logic
 Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
LICS'13, IEEE, pp 358367. 2013
PDF, Slides(PPTX), Reachability Logic, LICS'13, BIB  A Rewriting Logic Approach to Operational Semantics
 Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer
Information and Computation, Volume 207(2), pp 305340. 2009
PDF, Experiments, J.Inf.&Comp., BIB  AllPath 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 425440. 2014
PDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIB 
Unifying deductive program verification and (symbolic) model checking.
In our approach, there is no distinction between deductive verification and model checking.
These are just particular uses of our fixed and languageindependent 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 automatabased ones, where the automata encode both the program and the property to check.
This approach is particularly useful for explicitstate 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:
 AllPath 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 425440. 2014
PDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIB

Coinductive program verification.
Recall that conventional Hoarestyle program verification typically proves partial correctness of programs, that is, that a program satisfies its property if it terminates.
The nonterminating programs satisfy any property under partial correctness; in particular, a nonterminating program satisfies the property false.
Partial correctness should not be confused with total correctness, which means that the program terminates and it satisfies the desired property.
Termination is typically handled using different mechanisms (e.g., variants).
Sometimes researchers craft Hoare logics for total correctness, but those tend to be rather intricate.
Now, when partial correctness is sought to be proved, a very nice way to do it is by coinduction:
 Program Verification by Coinduction
 Brandon Moore and Grigore Rosu
Technical Report http://hdl.handle.net/2142/73177, February 2015
PDF, Matching Logic, DOI, BIB
 Formal Relationship between the Circularity proof rule and Coinduction.
 True concurrency with K.
 Rewritebased parsing.
 Fast execution engine.
 Semanticsbased compilation.
 Support full dynamic matching logic in K.
 Semanticsbased testcase generation.
 Symbolic execution framework.
 Symbolic model checking.
 Aggressive state/configurationreduction techniques. Graphisomorphism, alphaequivalence, userdefined abstractions.
 Languageindependent 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. Translationvalidation 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.
 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.
The original reachability logic proof systems that we proposed and proved sound and relatively complete, namely
worked only with language semantics defined using unconditional reachability rules and deriving onepath reachability rules. These are sufficient for deterministic language semantics in several frameworks, including in K. We tried hard to eliminate the "unconditional" and the "onepath" 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 onepath reachability rules:
Now thanks to this paper,
which shows that virtually all operational semantics approaches can be represented using rewriting with conditional rules, at least we have a general languageindependent (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 nondeterministic languages we typically want to prove allpath reachability.
Second, we were able to extend our results to prove allpath reachability, but only when the language semantics is defined using unconditional rules:
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 onepath and allpath 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.
So going through Coq is unnecessary.