Difference between revisions of "Open Problems and Challenges"

From FSL
Jump to: navigation, search
Line 241: Line 241:
 
'''Separation logic as a fragment of matching logic.'''
 
'''Separation logic as a fragment of matching logic.'''
 
</li>
 
</li>
 +
<pub id='rosu-schulte-2009-tr />
 
<pubbib id='rosu-stefanescu-2012-oopsla' />
 
<pubbib id='rosu-stefanescu-2012-oopsla' />
 
<pubbib id='rosu-2015-rta' />
 
<pubbib id='rosu-2015-rta' />

Revision as of 14:52, 31 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.
  2. 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).


  3. Sound and relatively complete reachability logic proof system with conditional rules (the challenge is the all-path).
  4. 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.


  5. Unifying deductive program verification and (symbolic) model checking.
  6. 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.


  7. Coinductive program verification.
  8. Recall that conventional Hoare-style program verification typically proves partial correctness of programs, that is, that a program satisfies its property if it terminates. The non-terminating programs satisfy any property under partial correctness; in particular, a non-terminating 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

    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 like a workbench, where one can use an interactive theorem prover like Coq or Isabelle with support for coinduction, and do proofs about programs 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 state-of-the-art 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 when real programming languages are concerned, 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 state-of-the-art, 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 state-of-the-art is simply unacceptable. Period.






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

  30. Novel verification methodologies.
  31. Our verification approach opens the door for novel verification methodologies. Aspects, runtime verification.

  32. K semantics to new real languages.
  33. Dwight's Python semantics needs to be published. Java 8. JavaScript ES6. WASM. SML, OCAML, Haskell, Ruby, C#, Go, etc.

  34. Separation logic as a fragment of matching logic.
  35. Self-organising assembly systems formally specified in Maude 
    Regina Frei, Traian Florin Serbanuta and Giovanna Di Marzo Serugendo
    J.AIHC, to appear. 2012
    PDF, DOI, BIB
    A Truly Concurrent Semantics for the K Framework Based on Graph Transformations 
    Traian Florin Serbanuta and Grigore Rosu
    ICGT'12, LNCS 7562, pp 294-310. 2012
    PDF, ICGT'12, Slides(PDF), BIB
    Maximal Causal Models for Sequentially Consistent Systems 
    Traian Florin Serbanuta, Feng Chen and Grigore Rosu
    RV'12, LNCS. 7687, pp 136-150. 2013
    PDF, Slides(PDF), 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
    Efficient, Expressive, and Effective Runtime Verification 
    Patrick Meredith
    PhD Thesis, University of Illinois, August 2012
    PDF, Slides(KEY), Slides(PDF), JavaMOP Project, BusMOP Project, RV-Predict Project, BIB
    Making Runtime Monitoring of Parametric Properties Practical 
    Dongyun Jin
    PhD Thesis, University of Illinois, August 2012
    PDF, Slides (PDF), JavaMOP, Sources, 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
    A Formal Semantics of C with Applications 
    Chucky Ellison
    PhD Thesis, University of Illinois, July 2012
    PDF, Slides, Project, 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
    Security-Policy Monitoring and Enforcement with JavaMOP 
    Soha Hussein, Patrick Meredith and Grigore Rosu
    PLAS'12, ACM, pp 3:1-3:11. 2012
    PDF, Slides(KEY), Slides(PDF), ACM, PLAS'12, BIB
    Executing Formal Semantics with the K Tool 
    David Lazar, Andrei Arusoaie, Traian Florin Serbanuta, Chucky Ellison, Radu Mereuta, Dorel Lucanu and Grigore Rosu
    FM'12, LNCS 7436, pp 267-271. 2012
    PDF, Slides(PDF), FM'12, DBLP, BIB
    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
    Defining the Undefinedness of C 
    Chucky Ellison and Grigore Rosu
    Technical Report http://hdl.handle.net/2142/30780, April 2012
    PDF, TR@UIUC, BIB
    Scalable Parametric Runtime Monitoring 
    Dongyun Jin, Patrick Meredith and Grigore Rosu
    Technical Report http://hdl.handle.net/2142/30757, April 2012
    PDF, TR@UIUC, BIB
    Efficient Parametric Runtime Verification with Deterministic String Rewriting 
    Patrick Meredith and Grigore Rosu
    Technical Report http://www.ideals.illinois.edu/handle/2142/30467, March 2012
    PDF, TR@UIUC, BIB
    K Framework Distilled 
    Dorel Lucanu, Traian Florin Serbanuta and Grigore Rosu
    WRLA'12, LNCS 7571, pp 31-53. 2012 Invited Paper
    PDF, Slides (PDF), WRLA'12, LNCS, BIB
    JavaMOP: Efficient Parametric Runtime Monitoring Framework 
    Dongyun Jin, Patrick Meredith, Choonghwan Lee and Grigore Rosu
    ICSE'12, IEEE, pp 1427-1430. 2012
    PDF, Demo Movie, TOOL ICSE'12, BIB
    Towards Categorizing and Formalizing the JDK API 
    Choonghwan Lee, Dongyun Jin, Patrick Meredith and Grigore Rosu
    Technical Report http://hdl.handle.net/2142/30006, March 2012
    PDF, TR@UIUC, BIB
    Test-Case Reduction for C Compiler Bugs 
    John Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison and Xuejun Yang
    PLDI'12, ACM, pp 335-346. 2012
    PDF, Slides(PPT), Project, ACM, PLDI'12, DBLP, BIB
    Semantics and Algorithms for Parametric Monitoring 
    Grigore Rosu and Feng Chen
    J.LMCS, Volume 8(1), pp 1-47. 2012
    PDF, MOP, J.LMCS, BIB
    The K Primer (version 2.5) 
    Traian Florin Serbanuta, Andrei Arusoaie, David Lazar, Chucky Ellison, Dorel Lucanu and Grigore Rosu
    Technical Report, January 2012
    PDF, K 2.5, BIB
    Making Maude Definitions more Interactive 
    Andrei Arusoaie, Traian Florin Serbanuta, Chucky Ellison and Grigore Rosu
    WRLA'12, LNCS 7571. 2012
    PDF, Slides (PDF), WRLA'12, BIB
    Recursive Proofs for Inductive Tree Data-Structures 
    Parthasarathy Madhusudan, Xiaokang Qiu and Andrei Stefanescu
    POPL'12, ACM, pp 123-136, 2012
    PDF, Slides(pptx), Slides(pdf), Dryad, ACM, POPL'12, BIB
    An Executable Formal Semantics of C with Applications 
    Chucky Ellison and Grigore Rosu
    POPL'12, ACM, pp 533-544. 2012
    PDF, Slides(PDF), Project, ACM, POPL'12, DBLP, BIB
    Matching Logic Rewriting: Unifying Operational and Axiomatic Semantics in a Practical and Generic Framework 
    Grigore Rosu and Andrei Stefanescu
    Technical Report http://hdl.handle.net/2142/28357, November 2011
    PDF, Matching Logic, TR@UIUC, , BIB
    A K-Based Formal Framework for Domain-Specific Modelling Languages 
    Vlad Rusu and Dorel Lucanu
    FoVeOOS'11, to appear
    PDF, FoVeOOS'11, BIB
    Context Transformers in the K Framework 
    Andrei Arusoaie and Traian Florin Serbanuta
    K'11. 2011. To appear
    PDF, Slides (PDF), K'11, BIB
    K Semantics for OCL — a Proposal for a Formal Definition for OCL 
    Vlad Rusu and Dorel Lucanu
    K'11. 2011. To appear
    PDF, Slides (PDF), K'11, BIB
    The Rewriting Logic Semantics Project: A Progress Report 
    Jose Meseguer and Grigore Rosu
    FCT'11, LNCS 6914, pp 1-37. Invited talk. 2011
    PDF, K Tool, FCT'11, BIB
    Improved Multithreaded Unit Testing 
    Vilas Jagannath, Milos Gligoric, Dongyun Jin, Qingzhou Luo, Grigore Rosu and Darko Marinov
    FSE'11, ACM, pp 223-233. 2011
    PDF, FSE'11, BIB
    Matching Logic: A New Program Verification Approach (NIER Track) 
    Grigore Rosu and Andrei Stefanescu
    ICSE'11, ACM, pp. 868-871. 2011
    PDF, Slides(pptx), Slides(pdf), Poster(pptx), Poster(pdf), Matching Logic, ACM, NIER ICSE'11, BIB
    Garbage Collection for Monitoring Parametric Properties 
    Dongyun Jin, Patrick Meredith, Dennis Griffith and Grigore Rosu
    PLDI'11, ACM, pp 415-424. 2011
    PDF, PLDI'11 slides(pptx), PLDI'11 slides(pdf), ACM, PLDI'11, JavaMOP, BIB
    Mining Parametric Specifications 
    Choonghwan Lee, Feng Chen and Grigore Rosu
    ICSE'11, ACM, pp 591-600. 2011
    PDF, Slides(pptx), ACM, ICSE'11, jMiner, BIB
    An Overview of the MOP Runtime Verification Framework 
    Patrick Meredith, Dongyun Jin, Dennis Griffith, Feng Chen and Grigore Rosu
    J.STTT, http://dx.doi.org/10.1007/s10009-011-0198-6
    PDF, J.STTT, BIB
    Path Directed Symbolic Execution in the K Framework 
    Irina Asavoae, Mihail Asavoae and Dorel Lucanu
    SYNACS'10, pp 133-141. 2010
    PDF, SYNACS'10, BIB
    Collecting Semantics under Predicate Abstraction in the K Framework 
    Irina Asavoae and Mihail Asavoae
    WRLA'10, LNCS 6381, pp 123-139, 2010
    DOI, BIB
    On Compiling Rewriting Logic Language Definitions into Competitive Interpreters 
    Michael Ilseman, Chucky Ellison and Grigore Rosu
    Technical Report http://hdl.handle.net/2142/17444, December 2010
    PDF, TR@UIUC, Compiler Webpage, BIB
    A Rewriting Approach to Concurrent Programming Language Design and Semantics 
    Traian Florin Serbanuta
    PhD Thesis, University of Illinois, December 2010
    PDF, Slides (PDF), K-Maude, TR@UIUC, BIB
    Matching Logic: A New Program Verification Approach 
    Grigore Rosu and Andrei Stefanescu
    UV'10. 2010
    PDF, Slides(pptx), Slides(pdf), Matching Logic, K framework, UV'10, BIB
    Subword balance, position indices and power sums 
    Arto Salomaa
    J. of CSS, Volume 76(8), pp 861-871. 2010
    J.CSS, BIB
    Runtime Verification with the RV System 
    Patrick Meredith and Grigore Rosu
    RV'10, LNCS 6418, pp 136-152. 2010
    PDF, Slides(PDF), Slides(PPT), Slides(KEY), RV'10, BIB
    Automating Coinduction with Case Analysis 
    Eugen-Ioan Goriac, Dorel Lucanu and Grigore Rosu
    ICFEM'10, LNCS 6447, pp 220-236. 2010
    PDF, LNCS, ICFEM'10, CIRC, BIB
    A Formal Executable Semantics of Verilog 
    Patrick Meredith, Michael Katelman, Jose Meseguer and Grigore Rosu
    Technical Report http://hdl.handle.net/2142/17079, July 2010
    PDF, TR@UIUC, BIB
    Matching Logic: An Alternative to Hoare/Floyd Logic 
    Grigore Rosu, Chucky Ellison and Wolfram Schulte
    AMAST'10, LNCS 6486, pp 142-162. 2010
    PDF, Slides(PPT), Slides(PDF), LNCS, AMAST'10, BIB
    K-Maude: A Rewriting Based Tool for Semantics of Programming Languages 
    Traian Florin Serbanuta and Grigore Rosu
    WRLA'10, LNCS 6381, pp 104-122. 2010
    PDF, Slides (PDF), K-Maude, LNCS, WRLA'10, BIB
    Ambient intelligence in self-organising assembly systems using the chemical reaction model 
    Regina Frei, Giovanna Di Marzo Serugendo and Traian Florin Serbanuta
    J. of Ambient Intelligence and Humanized Computing, Volume 1(3), pp 163-184. 2010
    J.AIHC, BIB
    P systems with control nuclei: The concept 
    Camelia Chira, Traian Florin Serbanuta and Gheorghe Stefanescu
    J.LAP, Volume 79(6), pp 326-333. 2010
    PDF, J.LAP, BIB
    An Overview of the K Semantic Framework 
    Grigore Rosu and Traian Florin Serbanuta
    J.LAP, Volume 79(6), pp 397-434. 2010
    PDF, Slides(PPTX), Slides(PDF), K Tool, J.LAP, BIB
    A Formal Executable Semantics of Verilog 
    Patrick Meredith, Michael Katelman, Jose Meseguer and Grigore Rosu
    MEMOCODE'10, IEEE, pp 179-188. 2010
    PDF, Slides(PDF), Sources, Verilog Semantics, IEEE, MEMOCODE'10, BIB
    On Parikh Matrices and Ambiguity 
    Virgil Nicolae Serbanuta
    PhD Thesis, University of Bucharest, April 2010
    PDF
    On Parikh Matrices and Ambiguity 
    Virgil Serbanuta
    PhD Thesis, University of Bucharest, April 2010
    PDF, BIB
    IMUnit: Improved Multithreaded Unit Testing 
    Vilas Jagannath, Milos Gligoric, Dongyun Jin, Grigore Rosu and Darko Marinov
    IWMSE'10, IEEE, pp 48-49. 2010
    PDF, IEEE, IWMSE'10, BIB
    Efficient Monitoring of Parametric Context-Free Patterns 
    Patrick Meredith, Dongyun Jin, Feng Chen and Grigore Rosu
    J. of ASE, Volume 17(2), pp 149-180. 2010
    PDF, J.ASE, BIB
    Efficient Formalism-Independent Monitoring of Parametric Properties 
    Feng Chen, Patrick Meredith, Dongyun Jin and Grigore Rosu
    ASE'09, IEEE/ACM, pp 383-394. 2009
    PDF, ASE'09 slides(KEY), ASE'09 slides(PDF), IEEE, ASE'09, BIB
    Circular Coinduction with Special Contexts 
    Dorel Lucanu and Grigore Rosu
    ICFEM'09, LNCS 5885, pp 639-659. 2009
    PDF, Slides(PDF), LNCS, ICFEM'09, BIB
    A Rewriting Logic Approach to Type Inference 
    Chucky Ellison, Traian Florin Serbanuta and Grigore Rosu
    WADT'08, LNCS 5486, pp 135-151. 2009
    PDF, Slides(PDF), LNCS, WADT'08, BIB
    Handling Mixed-Criticality in SoC-based Real-Time Embedded Systems 
    Rodolfo Pellizzoni, Patrick Meredith, Min-Young Nam, Mu Sun, Marco Caccamo and Lui Sha
    Emsoft'09, ACM, pp 235--244. 2009
    PDF, Slides(PPTX), ACM, Emsoft'09, BIB
    Runtime Verification of C Memory Safety 
    Grigore Rosu, Wolfram Schulte and Traian Florin Serbanuta
    RV'09, LNCS 5779, pp 132-151. 2009
    PDF, Slides (PDF), LNCS, RV'09, BIB
    Circular Coinduction: A Proof Theoretical Foundation 
    Grigore Rosu and Dorel Lucanu
    CALCO'09, LNCS 5728, pp 127-144. 2009
    Slides (PDF), LNCS, CALCO'09, DBLP, BIB
    From Rewriting Logic Executable Semantics to Matching Logic Program Verification 
    Grigore Rosu, Chucky Ellison and Wolfram Schulte
    Technical Report http://hdl.handle.net/2142/13159, July 2009
    PDF, TR@UIUC, BIB
    Matching Logic --- Extended Report 
    Grigore Rosu and Wolfram Schulte
    Technical Report UIUCDCS-R-2009-3026, January 2009
    TR@UIUC, BIB
    A Semantic Approach to Interpolation 
    Andrei Popescu, Traian Florin Serbanuta and Grigore Rosu
    J. of TCS, Volume 410(12-13), pp 1109-1128. 2009
    PDF, J.TCS, BIB
    Monitoring Oriented Programming - A Project Overview 
    Feng Chen, Dongyun Jin, Patrick Meredith, and Grigore Rosu
    ICICIS'09, pp 72-77. 2009
    PDF, ICICIS'09, BIB
    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
    On Parikh Matrices, Ambiguity, and Prints 
    Virgil Nicolae Șerbănuță
    IJFCS 20(1) pp 151-165. 2009
    PDF, DOI
    Charasteristic Words for Parikh Matrices 
    Arto Salomaa
    Automata, Formal Languages, and Related Topics, pp 117-127. 2009
    TR@TUCS, BIB
    Subword Occurrences, Parikh Matrices and Lyndon Images 
    Arto Salomaa and Sheng Yu
    IJFCS, Volume 21(1), pp 91-111. (2010)
    TR@TUCS, IJFCS, BIB
    Parametric Trace Slicing and Monitoring 
    Feng Chen and Grigore Rosu
    TACAS'09, LNCS 5505, pp 246-261. 2009.
    PDF, Slides (PPT), LNCS, TACAS'09, DBLP, BIB
    Dependent advice: A general approach to optimizing history-based Aspects 
    Eric Bodden, Feng Chen and Grigore Rosu
    AOSD'09, ACM, pp 3--14. 2009.
    PDF, ACM, AOSD'09, TR@ABC, BIB
    Some Alternatives to Parikh Matrices Using String Kernels 
    Alexander Clark and Chris Watkins
    Fundamenta Informaticae 84(3-4): 291-303 (2008)
    Electronic Edition, BIB
    On Subword Symmetry of Words 
    Anton Černý
    IJFCS 19(1): 243-250 (2008)
    DOI, BIB
    On inequalities between subword histories 
    Szilárd Zsolt Fazekas
    IJFCS 19(4): 1039-1047 (2008)
    DOI, BIB
    Towards a Module System for K 
    Mark Hills and Grigore Rosu
    WADT'08, LNCS 5486, pp 187-205. 2009
    PDF, LNCS, WADT'08, BIB
    Term-Generic Logic 
    Andrei Popescu and Grigore Rosu
    WADT'08, LNCS 5486, pp 290-307. 2009
    LNCS, WADT'08, BIB
    Hardware Runtime Monitoring for Dependable COTS-based Real-Time Embedded Systems 
    Rodolfo Pellizzoni, Patrick Meredith, Marco Caccamo and Grigore Rosu
    RTSS'08, IEEE, pp. 481-491. 2008
    PDF, Experiments, Slides(PPTX), IEEE, RTSS'08, BIB
    Defining and Executing P-systems with Structured Data in K 
    Traian Florin Serbanuta, Gheorghe Stefanescu and Grigore Rosu
    WMC'08, LNCS 5391, pp 374-393. 2009
    PDF, Slides (PDF), Experiments, LNCS, WMC'08, BIB
    Efficient Monitoring of Parametric Context-Free Patterns 
    Patrick Meredith, Dongyun Jin, Feng Chen and Grigore Rosu
    ASE'08, IEEE/ACM, pp 148-157. 2008 ACM Sigsoft Distinguished Paper
    PDF, Experiments, ASE'08 slides(KEY), ASE'08 slides(MOV), ASE'08 slides(PPT), IEEE, ASE'08, BIB
    Subword histories and associated matrices 
    Arto Salomaa
    J. of TCS 407(1-3): 250-257 (2008)
    DOI, BIB
    Mining Parametric State-Based Specifications from Executions 
    Feng Chen and Grigore Rosu
    Technical report UIUCDCS-R-2008-3000, September 2008
    PDF, BIB
    A Rewriting Logic Approach to Static Checking of Units of Measurement in C 
    Mark Hills, Feng Chen and Grigore Rosu
    RULE'08, ENTCS, to appear, 2008
    PDF, RULE'08 slides, RULE'08, BIB
    Monitoring IVHM Systems using a Monitor-Oriented Programming Framework 
    Sudipto Ghoshal, Solaiappan Manimaran, Grigore Rosu, Traian Florin Serbanuta, and Gheorghe Stefanescu
    LFM 2008
    PDF, Slides (PPT), LFM'08, BIB
    jPredictor: A Predictive Runtime Analysis Tool for Java 
    Feng Chen and Traian Florin Serbanuta and Grigore Rosu
    ICSE'08, ACM, pp. 221-230. 2008
    PDF, Slides(PDF), DOI, ICSE'08, BIB
    A Rewriting Logic Approach to Defining Type Systems 
    Chucky Ellison
    Master's Thesis
    PDF, TR@UIUC, BIB
    A Rewriting Logic Approach to Type Inference 
    Chucky Ellison, Traian Florin Serbanuta and Grigore Rosu
    Technical report UIUCDCS-R-2008-2934, March 2008
    PDF, TR@UIUC, BIB
    Parikh matrices and amiable words 
    Adrian Atanasiu, Radu Atanasiu and Ion Petre
    J. of TCS 390(1): 102-109 (2008)
    DOI, BIB
    On Compiling Structured Interactive Programs with Registers and Voices 
    Cezara Dragoi and Gheorghe Stefanescu
    SOFSEM'08, LNCS 4910, pages 259-270
    LNCS, BIB
    High-level Structured Interactive Programs with Registers and Voices 
    Alexandru Popa, Alexandru Sofronia and Gheorghe Stefanescu
    J.UCS (Vol.13)(No.11), 2007, pages 1722-1754
    Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns -- 
    Grigore Rosu, Feng Chen and Thomas Ball
    RV'08, LNCS 5289, pp 51-68, 2008
    PDF, RV'08, BIB
    Pluggable Policies for C 
    Mark Hills, Feng Chen and Grigore Rosu
    Technical Report UIUCDCS-R-2008-2931, January 2008
    PDF, TR@UIUC, BIB
    Memory Representations in Rewriting Logic Semantics Definitions 
    Mark Hills
    WRLA'08, ENTCS, to appear, 2008
    PDF, WRLA'08 slides, WRLA'08, BIB
    On fairness of D0L systems 
    Anton Černý
    Discrete Applied Mathematics 155(3), pp 1769-1773. 2007
    DOI, BIB
    Comparing Subword Occurrences in Binary D0L Sequences 
    Arto Salomaa
    IJFCS 18(6): 1395-1406. 2007
    DOI, BIB
    K: A Rewriting-Based Framework for Computations -- Preliminary version 
    Grigore Rosu
    Technical report UIUCDCS-R-2007-2926 and UILU-ENG-2007-1827, December 2007
    PDF, ZIP, TR@UIUC, BIB
    AGAPIA v0.1: A Programming Language for Interactive Systems and its Typing System 
    Cezara Dragoi and Gheorghe Stefanescu
    FInCo'07
    PDF, FinCo
    Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns -- 
    Grigore Rosu,Feng Chen and Thomas Ball
    Technical report UIUCDCS-R-2007-2908, October 2007
    PDF, BIB
    A K Definition of Scheme 
    Patrick Meredith, Mark Hills and Grigore Rosu
    Technical Report UIUCDCS-R-2007-2907, October 2007
    PDF, TR@UIUC, BIB
    Subword Balance in Binary Words, Languages and Sequences 
    Arto Salomaa
    Fundamenta Informaticae, 75(1-4):469-482 (2007)
    IOSPRESS, BIB
    Binary Amiable Words 
    Adrian Atanasiu
    IJFCS 18(2): 387-400 (2007)
    DOI, BIB
    Effective Predictive Runtime Analysis Using Sliced Causality and Atomicity 
    Feng Chen, Traian Florin Serbanuta and Grigore Rosu
    Technical report UIUCDCS-R-2007-2905, October 2007
    PDF, TR@UIUC, BIB
    An Executable Rewriting Logic Semantics of K-Scheme 
    Patrick Meredith, Mark Hills and Grigore Rosu
    8th Workshop on Scheme and Functional Programming, Technical Report DIUL-RT-0701, pp. 91-103, September 2007
    PDF, SCHEME'07, BIB
    A Rewriting Approach to the Design and Evolution of Object-Oriented Languages 
    Mark Hills and Grigore Rosu
    OOPSLA'07 Companion, ACM Press, pp 827-828. 2007
    PDF, OOPSLA'07 poster, ACM, OOPSLA'07, BIB
    A Rewriting Approach to the Design and Evolution of Object-Oriented Languages 
    Mark Hills and Grigore Rosu
    Technical Report Bericht-Nr. 2007-7, pp. 23-26, July 2007
    PDF, ECOOP'07 Doctoral Symposium slides, ECOOP'07 Doctoral Symposium, BIB
    On RDBMS-Integrated Disk-Based Architecture for Managing Massive Dormant Data in a Compressed Format 
    Miroslav Dzakovic and Chucky Ellison
    SNAPI'07, IEEE
    PDF, IEEE, BIB
    MOP: An Efficient and Generic Runtime Verification Framework 
    Feng Chen and Grigore Rosu
    OOPSLA'07, ACM press, pp 569-588. 2007
    PDF, OOPSLA'07 slides, ACM, OOPSLA'07, DBLP, TR@UIUC, BIB
    A Rewriting Logic Approach to Operational Semantics -- Extended Abstract 
    Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer
    SOS'07, ENTCS 192(1), pp 125-141. 2007
    PDF, Slides (PPT), ENTCS, SOS'07, BIB
    CIRC: A Circular Coinductive Prover 
    Dorel Lucanu and Grigore Rosu
    CALCO'07, LNCS 4624, pp 372-378. 2007
    PDF, CIRC webpage, CALCO'07, BIB
    Parametric and Sliced Causality 
    Feng Chen and Grigore Rosu
    CAV'07, LNCS 4590, pp 240 - 253, 2007
    PDF, CAV'07 slides, CAV'07, TR@UIUC, BIB
    KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis 
    Mark Hills and Grigore Rosu
    RTA'07, LNCS 4533, pp 246-256. 2007
    PDF, RTA'07 slides, LNCS, RTA'07, BIB
    On Formal Analysis of OO Languages using Rewriting Logic: Designing for Performance 
    Mark Hills and Grigore Rosu
    FMOODS'07, LNCS 4468, pp 107-121. 2007
    PDF, FMOODS'07 slides, LNCS, FMOODS'07, BIB
    On Safety Properties and Their Monitoring 
    Grigore Rosu
    Technical report UIUCDCS-R-2007-2850, February 2007
    PDF, ZIP, TR@UIUC, BIB
    An Effective Algorithm for the Membership Problem for Extended Regular Expressions 
    Grigore Rosu
    FOSSACS'07, LNCS 4423, pp 332-345, 2007
    PDF, FOSSACS'07, BIB
    The Rewriting Logic Semantics Project 
    Jose Meseguer and Grigore Rosu
    J. of TCS, Volume 373(3), pp 213-237. 2007
    PDF, J.TCS, BIB
    Subword conditions and subword histories 
    Arto Salomaa and Sheng Yu
    Information and Computation 204(12): 1741-1755, 2006
    DOI, BIB
    Independence of certain quantities indicating subword occurrences 
    Arto Salomaa
    J. of TCS 362(1-3): 222-231 (2006)
    DOI, BIB
    Towards a Floyd logic for interactive rv-systems 
    Gheorghe Stefanescu
    ICCP'06, pages 169-178, September 2006
    PDF
    Structured programming for interactive rv-systems 
    Cezara Dragoi and Gheorghe Stefanescu
    Preprint IMAR 9/2006
    PDF
    Towards a Hoare logic for structured interactive rv-programs 
    Cezara Dragoi and Gheorghe Stefanescu
    Preprint IMAR 10/2006
    PDF
    Implementation and verification of ring termination detection protocols using structured rv-programs 
    Cezara Dragoi and Gheorghe Stefanescu
    Annals of University of Bucharest, Mathematics-Informatics Series, LV(2006)
    PDF
    Interactive Systems with Registers and Voices 
    Gheorghe Stefanescu
    Fundamenta Informaticae (73), 2006, pages 285--306
    PDF, IOSPRESS, Pisa'07 Slides, BIB
    A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters 
    Mark Hills, Traian Florin Serbanuta and Grigore Rosu
    WRLA'06, ENTCS 176(4), pp. 215-231. 2007
    PDF, Experiments, ENTCS, WRLA'06, BIB
    K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation 
    Grigore Rosu
    Technical report UIUCDCS-R-2006-2802, December 2006
    PDF, TR@UIUC, BIB
    A Rewriting Based Approach to OO Language Prototyping and Design 
    Mark Hills and Grigore Rosu
    Technical Report UIUCDCS-R-2006-2786, October 2006
    PDF, TR@UIUC, BIB
    KOOL: A K-based Object-Oriented Language 
    Mark Hills and Grigore Rosu
    Technical Report UIUCDCS-R-2006-2779, October 2006
    PDF, TR@UIUC, BIB
    MOP: Reliable Software Development using Abstract Aspects 
    Feng Chen and Grigore Rosu
    Technical report UIUCDCS-R-2006-2776, October 2006
    PDF, TR@UIUC, BIB
    Computationally Equivalent Elimination of Conditions - extended abstract 
    Traian Florin Serbanuta and Grigore Rosu
    RTA'06, LNCS 4098, pp 19-34. 2006
    PDF, Slides (PPT), Experiments, LNCS, RTA'06, DBLP, BIB
    On Some Problems of Mateescu Concerning Subword Occurrences 
    Cunsheng Ding and Arto Salomaa
    Fundamenta Informaticae 73(1-2): 65-79 (2006)
    IOSPRESS, BIB
    Injectivity of the Parikh matrix mappings revisited 
    Virgil Nicolae Șerbănuță and Traian Florin Serbanuta
    Fundamenta Informaticae, Volume 73(1-2), pp. 265-283. 2006
    PDF, IOSPRESS, BIB
    GFOL: a Term-Generic Logic for Defining Lambda-Calculi 
    Andrei Popescu and Grigore Rosu
    Technical Report UIUCDCS-R-2006-2756, July 2006
    PDF, TR@UIUC, BIB
    Discovering Likely Method Specifications 
    Nikolai Tillmann and Feng Chen and Wolfram Schulte
    ICFEM'06, to appear in LNCS, 2006
    PDF, ICFEM'06, BIB
    Equality of Streams is a Pi_2^0-Complete Problem 
    Grigore Rosu
    ICFP'06, ACM, 2006
    PDF, ICFP'06 Slides, ACM, ICFP'06, BIB
    Complete Categorical Deduction for Satisfaction as Injectivity 
    Grigore Rosu
    Festschrift in Honor of Joseph Goguen, LNCS 4060, pp 157-172. 2006.
    PDF, Goguen's Festschrift slides, LNCS, Goguen's Festschrift, Goguen's Webpage, BIB
    Allen Linear (Interval) Temporal Logic -Translation to LTL and Monitor Synthesis- 
    Grigore Rosu and Saddek Bensalem
    CAV'06, LNCS 4144, pp 263-277, 2006
    PDF, CAV'06, CAV'06 Slides, BIB
    Parametric and Termination-Sensitive Control Dependence - Extended Abstract 
    Feng Chen and Grigore Rosu
    SAS'06, LNCS 4134, pp 387-404. 2006.
    PDF, LNCS, SAS'06, BIB
    Haskell-RL: An Equational Specification of Haskell in Maude 
    Andrew Bennett
    MS CS Thesis Submission
    PDF, semantics
    A Rewrite Logic Approach to Semantic Definition, Design and Analysis of Object-Oriented Languages 
    Feng Chen, Mark Hills and Grigore Rosu
    Technical Report UIUCDCS-R-2006-2702, March 2006
    PDF, TR@UIUC, BIB
    Parametric and Termination-Sensitive Control Dependence 
    Feng Chen and Grigore Rosu
    Technical report UIUCDCS-R-2006-2712, April 2006
    PDF, TR@UIUC, BIB
    Predicting Concurrency Errors at Runtime using Sliced Causality 
    Feng Chen and Grigore Rosu
    Technical report UIUCDCS-R-2006-2965, 2006.
    PDF, TR@UIUC, BIB
    A Semantic Approach to Interpolation 
    Andrei Popescu, Traian Florin Serbanuta and Grigore Rosu
    FOSSACS'06, LNCS 3921, pp 307-321. 2006
    PDF, Slides (PDF), LNCS, FOSSACS '06, DBLP, BIB
    Static Analysis to Enforce Safe Value Flow in Embedded Control Systems 
    Sumant Kowshik, Grigore Rosu and Lui Sha
    DSN'06, IEEE, pp 23-34. 2006.
    PDF, DSN'06 Slides, IEEE, DSN'06, BIB
    Connections between subwords and certain matrix mappings 
    Arto Salomaa
    J. of TCS 340(1): 188-203 (2005)
    DOI, BIB
    Efficient Monitoring of Omega-Languages 
    Marcelo d'Amorim and Grigore Rosu
    CAV'05, LNCS 3576, pp 364 - 378. 2005.
    PDF, LNCS, CAV'05, DBLP, BIB
    On the Injectivity of Parikh Matrix Mappings 
    Arto Salomaa
    Fundamenta Informaticae 64(1-4): 391-404 (2005)
    IOSPRESS, BIB
    On Some Problems of Mateescu Concerning Subword Occurrences 
    Cunsheng Ding and Arto Salomaa
    Technical Report TUCS-TR-701, August 2005
    Tech. Report's page, BIB
    On Languages Defined by Numerical Parameters 
    Arto Salomaa
    Technical Report TUCS-TR-663. 2005
    Tech. Report's page, BIB
    Behavioral Extensions of Institutions 
    Andrei Popescu and Grigore Rosu
    CALCO'05, LNCS 3629, pp. 331-347. 2005
    PDF, CALCO'05 Slides, LNCS , CALCO '05, DBLP, BIB
    Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP 
    Feng Chen, Marcelo d'Amorim and Grigore Rosu
    RV'05, ENTCS 144, issue 4, pp 3-20. 2005.
    PDF, ENTCS, RV'05, DBLP, BIB
    Predicting Concurrency Errors at Runtime using Sliced Causality 
    Feng Chen and Grigore Rosu
    Technical report UIUCDCS-R-2005-2660, 2005.
    PDF, TR@UIUC, BIB
    Java-MOP: A Monitoring Oriented Programming Environment for Java 
    Feng Chen and Grigore Rosu
    TACAS'05, LNCS 3440, pp 546-550. 2005.
    PDF, LNCS, TACAS'05, DBLP, BIB
    Automatic and Precise Dimensional Analysis 
    Marcelo d'Amorim, Mark Hills, Feng Chen and Grigore Rosu
    Technical Report UIUCDCS-R-2005-2668, December 2005
    PDF, Sources, TR@UIUC, BIB
    K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation 
    Grigore Rosu
    Technical Report UIUCDCS-R-2005-2672, December 2005
    PDF, Experiments, BIB
    An Executable Semantic Definition of the Beta Language using Rewriting Logic 
    Mark Hills, T. Baris Aktemur and Grigore Rosu
    Technical Report UIUCDCS-R-2005-2650, November 2005
    PDF, TR@UIUC, BIB
    Rewriting-based Techniques for Runtime Verification 
    Grigore Rosu and Klaus Havelund
    J.ASE, Volume 12(2), pp 151-197. 2005
    PDF, J.ASE, DBLP, BIB
    The Rewriting Logic Semantics Project 
    Jose Meseguer and Grigore Rosu
    SOS'05, ENTCS 156, pp. 27-56. 2006
    PDF, SOS'05, BIB
    An Effective Algorithm for the Membership Problem for Extended Regular Expressions 
    Grigore Rosu
    Technical Report UIUCDCS-R-2005-2694, August 2005
    PDF, Technical Report @ UIUC, BIB
    Similarity Convergence in Residuated Structures 
    George Georgescu and Andrei Popescu
    Logic J.IGPL 13(4): 389-413 (2005)
    Logic J.IGPL, DBLP, BIB
    Lukasiewicz-Moisil Relation Algebras 
    Andei Popescu
    Studia Logica 81(2): 167-189 (2005)
    Studia Logica, DBLP, BIB
    Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools 
    Jose Meseguer and Grigore Rosu
    IJCAR'04, LNCS 3097, pp 1-44. 2004
    PDF, Maude-code, LNCS, IJCAR'04, BIB
    Interactive Systems with Registers and Voices 
    Gheorghe Stefanescu
    Draft, National University of Singapore (SoC/NUS), July 2004
    PDF, SoC/NUS
    Some characterizations of Parikh matrix equivalent binary words 
    S. Fosse and G. Richomme
    Information Processing Letters 92(2):77-82 (2004)
    DOI, BIB
    Efficient Monitoring of Safety Properties 
    Klaus Havelund and Grigore Rosu
    J. of STTT, Volume 6(2), pp 158-173. 2004
    PDF, J.STTT, BIB
    Algebraic Aspects of Parikh Matrices 
    Alexandru Mateescu
    Theory Is Forever, LNCS 3113: 170-180 (2004)
    LNCS, BIB
    Matrix Indicators For Subword Occurrences And Ambiguity 
    Alexandru Mateescu and Arto Salomaa
    IJFCS 15(2): 277-292 (2004)
    IJFCS, Technical Report, BIB
    Subword histories and Parikh matrices 
    Alexandru Mateescu and Arto Salomaa and Sheng Yu
    JCSS 68(1): 1-21 (2004)
    JCSS, BIB
    Pruning Interference and Ready Dependence for Slicing Concurrent Java Programs 
    Venkatesh Prasad Ranganath and John Hatcliff
    CC 2004, LNCS Volume 2985, pp. 39 - 56
    Monitoring-Oriented Programming: A Tool-Supported Methodology for Higher Quality Object-Oriented Software 
    Feng Chen, Marcelo d'Amorim and Grigore Rosu
    Technical Report UIUCDCS-R-2004-2420, 2004.
    PDF, TR@UIUC, BIB
    A Formal Monitoring-based Framework for Software Development and Analysis 
    Feng Chen and Marcelo d'Amorim and Grigore Rosu
    ICFEM'04, LNCS 3308, pp 357 - 373. 2004.
    PDF, LNCS, ICFEM'04, DBLP, BIB
    Formal Analysis of Java Programs in JavaFAN 
    Azadeh Farzan, Feng Chen, Jose Meseguer and Grigore Rosu
    CAV'04, LNCS 3114, pp 501 - 505. 2004.
    PDF, LNCS, CAV'04, DBLP, BIB
    A general approach to fuzzy concepts 
    Andrei Popescu
    Math. Log. Q. 50(3): 265-280 (2004)
    Math. Log. Q., DBLP, BIB
    An Orchestration Language for Parallel Objects 
    L.V. Kale, Mark Hills and Chao Huang
    LCR'04
    PDF, PPL Paper Page, LCR'04, BIB
    From Conditional to Unconditional Rewriting 
    Grigore Rosu
    WADT'04, LNCS 3423, pp 218-233. 2004
    PDF, LNCS, WADT'04, Experiments, PDF - Original submission, WADT'04 slides, BIB
    From Conditional to Unconditional Rewriting 
    Grigore Rosu
    Technical Report UIUCDCS-R-2004-2471, August 2004
    PDF, Technical reports' page, Experiments, BIB
    Behavioral Abstraction is Hiding Information 
    Grigore Rosu
    J. of TCS, Volume 327(1-2), pp 197-221. 2004
    PDF, J.TCS, BIB
    Extending Parikh Matrices 
    Traian Florin Serbanuta
    J. of TCS, Volume 310(1), pp 233-246. 2004
    PDF, J.TCS, DBLP, BIB
    Non-dual fuzzy connections 
    George Georgescu and Andrei Popescu
    Arch. Math. Log. 43(8): 1009-1039 (2004)
    Arch. Math. Log., DBLP, BIB
    Non-commutative fuzzy structures and pairs of weak negations 
    George Georgescu and Andrei Popescu
    Fuzzy Sets and Systems 143(1): 129-155 (2004)
    Fuzzy Sets and Systems, DBLP, BIB
    Counting (scattered) Subwords 
    Arto Salomaa
    B. of EATCS 81: 165-179 (2003)
    BIB
    Certifying Measurement Unit Safety Policy 
    Grigore Rosu and Feng Chen
    ASE'03, IEEE, pp. 304 - 309. 2003.
    PDF, IEEE, ASE'03, BIB
    Rule-Based Analysis of Dimensional Safety 
    Feng Chen and Grigore Rosu and Ram Prasad Venkatesan
    RTA'03, LNCS 2706, pp197 - 207. 2003.
    PDF, LNCS, RTA'03, DBLP, BIB
    Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation 
    Feng Chen and Grigore Rosu
    RV'03, ENTCS 89, issue 2, pp 108 - 127. 2003.
    PDF, ENTCS, RV'03, DBLP, BIB
    CS322 - Programming Language Design: Lecture Notes 
    Grigore Rosu
    Technical Report UIUCDCS-R-2003-2897, December 2003
    PDF, TR @ UIUC, BIB
    Non-commutative fuzzy Galois connections 
    George Georgescu and Andrei Popescu
    Soft Comput. 7(7): 458-467 (2003)
    Soft Comput., DBLP, BIB
    Inductive Behavioral Proofs by Unhiding 
    Grigore Rosu
    CMCS'03, ENTCS 82(1). 2003
    PDF, ENTCS, CMCS'03, Experiments, DBLP, BIB
    On the Injectivity of the Parikh Matrix Mapping 
    Adrian Atanasiu, Carlos Martin-Vide and Alexandru Mateescu
    Fundamenta Informaticae 49(4): 289-299 (2002)
    BIB
    An Architecture-Based Approach for Component-Oriented Development 
    Feng Chen and Qianxiang Wang and Hong Mei and Fuqing Yang
    COMPSAC'02, IEEE press, pp 450 - 455. 2002
    PDF, BIB
    ABC/ADL: An ADL Supporting Component Composition 
    Hong Mei and Feng Chen and Qianxiang Wang and Yaodong Feng
    ICFEM'02, LNCS 2459, pp 38 - 47. 2002
    PDF, BIB
    Using Application Server To Support Online Evolution 
    Qianxiang Wang and Feng Chen and Hong Mei and Fuqing Yan
    ICSM'02, IEEE press, pp. 131-140. 2002
    PDF, BIB
    Concept lattices and similarity in non-commutative fuzzy logic 
    George Georgescu and Andrei Popescu
    Fundam. Inform. 53(1): 23-54 (2002)
    Fundam. Inform., DBLP, BIB
    Codifiable languages and the Parikh matrix mapping 
    Adrian Atanasiu, Carlos Martin-Vide and Alexandru Mateescu
    JUCS 7(9): 783–793 (2001)
    JUCS, BIB
    A sharpening of the Parikh mapping 
    Alexandru Mateescu, Arto Salomaa, Kai Salomaa and Sheng Yu
    ITA 35(6): 551-564 (2001)
    ITA, BIB
    Hybrid natural language processing in a customer-care environment 
    David Reitter, Stefan Covaci, Florin Oltean, Catalin Bacanu and Traian Florin Serbanuta
    TaCoS'01. 2001.
    PDF, citeseer, TaCoS, BIB
    Hidden Logic 
    Grigore Rosu
    PhD Thesis, University of California at San Diego
    PDF, Thesis@UCSD, BIB
    On an Extension of the Parikh Mapping 
    Alexandru Mateescu, Arto Salomaa, Kai Salomaa and Sheng Yu
    Technical Report TUCS-TR-364, September 2000
    Tech. Report's page, citeseer, BIB
    Race Condition Detection For Debugging Shared-Memory Parallel Programs 
    Robert Harry Benson Netzer
    Wisc. Ph.D. Thesis, 1991
    Programming Languages and Lambda Calculi 
    Matthias Felleisen and Matthew Flatt
    book draft, 1989, 2003, 2006
    PDF, 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, DOI, OOPSLA'12, BIB

    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


  36. Verification of real-time languages, WCET verification.
Personal tools
Namespaces

Variants
Actions
Navigation