# Difference between revisions of "Open Problems and Challenges"

(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
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
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
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
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
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
Term-Generic Logic
Andrei Popescu and Grigore Rosu
WADT'08, LNCS 5486, pp 290-307. 2009
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
Deﬁning 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
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
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-
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
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
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
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.