Difference between revisions of "ERE Monitoring Algorithm"

From FSL
Jump to: navigation, search
Line 10: Line 10:
 
More information can be found in the following paper:
 
More information can be found in the following paper:
  
<pub id=rosu-2007-fossacs />
+
<pub /chen-rosu-2003-rv />
 
+
<pub id=rosu-2005-tr-b />
+

Revision as of 04:11, 30 October 2008

Under construction!

Regular expressions can be easily understood by ordinary software engineers and programmers, as shown by the immense interest in and the success of scripting languages like Perl, based essentially on regular expression pattern matching. We believe that regular expressions provide an elegant and powerful specification language also for monitoring requirements, because an execution trace of a program is in fact a string of states. Extended regular expressions (EREs) add complementation to regular expressions, which brings additional benefits by allowing one to specify patterns that must not occur during an execution. Complementation gives one the power to express patterns on strings non-elementarily more compactly. Generating optimal ERE monitors is highly non-trivial and the interested reader should refer to the below papers. One important observation about the use of ERE in the context of runtime verification is that ERE patterns are often used to describe buggy patterns instead of desired properties.

Publications

More information can be found in the following paper:

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

Personal tools
Namespaces

Variants
Actions
Navigation