Difference between revisions of "Open Problems and Challenges"

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.

Dynamic matching logic.

Currently (Jan 2016), we are framing matching logic as a static logic, that is, as one for reasoning about program configurations at a particular place in the execution of a program:

Matching Logic --- Extended Abstract: Grigore Rosu
RTA'15, Leibniz International Proceedings in Informatics (LIPIcs) 36, pp 5-21. 2015
PDF, Slides(PPTX), Matching Logic, DOI, RTA'15, BIB

For dynamic properties we use reachability logic:

All-Path Reachability Logic: Andrei Stefanescu and Stefan Ciobaca and Radu Mereuta and Brandon Moore and Traian Florin Serbanuta and Grigore Rosu
RTA'14, LNCS 8560, pp 425-440. 2014
PDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIB

One-Path Reachability Logic: Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
LICS'13, IEEE, pp 358-367. 2013
PDF, Slides(PPTX), Reachability Logic, LICS'13, BIB

However, both one-path and all-path reachability rules are particular formulae in a more general dynamic matching logic, which extends matching logic with two constructs: a modal next construct and a usual fixed-point mu construct. The resulting logic is expected to be sound and relatively complete; the relativity comes from the fact that we will want to fix a model of configurations, same like in reachability logic, to enable the use of SMT solvers for domain reasoning. Once defined, then we should be able to prove the reachability logic proof system rules as theorems, thus modulo

From Hoare Logic to Matching Logic Reachability: Grigore Rosu and Andrei Stefanescu
FM'12, LNCS 7436, pp 387-402. 2012
PDF, Slides(pptx), Slides(pdf), Matching Logic, FM'12, , BIB

obtaining that dynamic matching logic generalizes Hoare logic mechanically. We should also be able to prove that dynamic matching logic similarly generalizes dynamic logic. The point of these generalizations is that Hoare or dynamic logic are basically "design patterns" to be manually crafted for each language separately, while dynamic matching logic is one fixed logic for all languages; each language is a particular set of axioms, which can be used in combination with a language-independent fixed proof system to derive any dynamic property for the language. In our view, that is how program reasoning/verification should be done, using one language-independent and powerful logic, and not to craft a specific logic for each specific language (which is what Hoare/dynamic/separation logic advocate).

Sound and relatively complete reachability logic proof system with conditional rules (the challenge is the all-path).

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.

Unifying deductive program verification and (symbolic) model checking.

In our approach, there is no distinction between deductive verification and model checking. These are just particular uses of our fixed and 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.

Coinductive program verification.

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.

Formal Relationship between the Circularity proof rule and Coinduction.
True concurrency with K.
Rewrite-based parsing.
Fast execution engine.
Semantics-based compilation.
Support full dynamic matching logic in K.
Semantics-based test-case generation.
Symbolic execution framework.
Symbolic model checking.
Aggressive state/configuration-reduction techniques. Graph-isomorphism, alpha-equivalence, user-defined abstractions.
Language-independent infrastructure for program equivalence.
C program portability checking.
Verifying compiler optimizations and even complete compiler. LLVM.
Strategy language.
Systematic comparison of K with other operational approaches. K evolved from other approaches, systematically analyzing their advantages and disadvantages, and keeping the advantages and eliminating the disadvantages. This is partly explained in my book draft, but it needs to be also published as a conference/journal paper, for wider dissemination. Indeed, we have encountered many scientists who seem to think that K is some new theoretical development based on new principles. Well, sorry to disappoint, but K is an engineering endeavor attempting to get the best of the ideas developed by the formal semantics community over the last four decades, avoiding their limitations. The main novelties of K, besides its unique notation, are: (1) its concurrent semantics, which allows for true concurrency even in the presence of sharing; and (2) its configuration abstraction mechanism which is the key for more modular language definitions.
Configuration abstraction.
Defining/Implementing language translators/compilers in K. Translation-validation style, or provably correct style, or both.
Translations from K to other languages or formalisms. Maude, OCAML, Coq, Haskell, LLVM, etc. Both interpreters and compilers.
Coq certification of proofs using K framework.
Matching logic proof checker/certifier.

So going through Coq is unnecessary.

Novel verification methodologies.

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

K semantics to new real languages.

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

Separation logic as a fragment of matching logic.

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
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: 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

Verification of real-time languages, WCET verification.

@@ Line 241: / Line 241: @@
 '''Separation logic as a fragment of matching logic.'''
 </li>
+<pub id='rosu-schulte-2009-tr />
 <pubbib id='rosu-stefanescu-2012-oopsla' />
 <pubbib id='rosu-2015-rta' />

Difference between revisions of "Open Problems and Challenges"

Revision as of 14:52, 31 January 2016

Personal tools

Namespaces

Variants

Views

Actions

Search

Navigation