 IDEALS Home
 →
 Browse by Author
Browse by Author "Rosu, Grigore"
Now showing items 120 of 94

Rosu, Grigore; Bensalem, Saddek (200601)The relationship between two well established formalisms for temporal reasoning is first investigated, namely between Allen's interval algebra (or Allen's temporal logic, abbreviated \ATL) and linear temporal logic (\LTL). ...
application/pdf
PDF (298kB) 
d'Amorim, Marcelo; Hills, Mark; Chen, Feng; Rosu, Grigore (200512)The loss of NASA's Mars climate orbiter is evidence of the importance of units of measurement as a safety policy for software in general and for scientific applications in particular. In this paper we present a static ...
application/pdf
PDF (244kB) 
Popescu, Andrei; Rosu, Grigore (200505)We show that any institution I satisfying some reasonable conditions can be transformed into another institution, Ib, which captures formally and abstractly the intuitions of adding support for behavioral equivalence and ...
application/pdf
PDF (332kB) 
Rosu, Grigore; Stefanescu, Andrei (201204)This paper presents a verification framework that is parametric in a (trusted) operational semantics of some programming language. The underlying proof system is languageindependent and consists of eight proof rules. ...
application/pdf
PDF (343kB) 
Rosu, Grigore; Stefanescu, Andrei (201208)This paper presents a verification framework that is parametric in a (trusted) operational semantics of some programming language. The underlying proof system is languageindependent and consists of eight proof rules. The ...
application/pdf
PDF (346kB) 
Lucanu, Dorel; Rosu, Grigore (200902)Coinductive proofs of behavioral equivalence often require human ingenuity, in that one is expected to provide a "good" relation extending one's goal with additional lemmas, making automation of coinduction a challenging ...
application/pdf
PDF (260kB) 
Rosu, Grigore; Lucanu, Dorel (200902)Several algorithmic variants of circular coinduction have been proposed and implemented during the last decade, but a proof theoretical foundation of circular coinduction in its full generality is still missing. This paper ...
application/pdf
PDF (223kB) 
Rosu, Grigore; Lucanu, Dorel (200902)Several algorithmic variants of circular coinduction have been proposed and implemented during the last decade, but a proof theoretical foundation of circular coinduction in its full generality is still missing. This paper ...
application/pdf
PDF (223kB) 
Serbanuta, Traian Florin; Rosu, Grigore (200602)An automatic and easy to implement transformation of conditional term rewrite systems into computationally equivalent unconditional term rewrite systems is presented. No special support is needed from the underlying ...
application/pdf
PDF (330kB) 
Rosu, Grigore (200312)This report contains the complete lecture notes for CS322, Programming Language Design, taught by Grigore Rosu in the Fall 2003 semester at the University of Illinois at Urbana Champaign. This large PDF document has been ...
application/pdf
PDF (2MB) 
Ellison, Chucky M.; Rosu, Grigore (20120427)This paper investigates undefined behavior in C and offers a few simple techniques for operationally specifying such behavior formally. A semanticsbased undefinedness checker for C is developed using these techniques, as ...
application/pdf
PDF (257kB) 
Sen, Koushik; Rosu, Grigore; Agha, Gul A. (200412)A generalized predictive analysis technique is proposed for detecting violations of safety properties from apparently successful executions of multithreaded programs. Specifically, we provide an algorithm to monitor ...
application/pdf
PDF (208kB) 
Rosu, Grigore (200508)By adding the complement operator (\neg), extended regular expressions ({\ERE}) can encode regular languages nonelementarily more succinctly than regular expressions. The {\ERE} membership problem asks whether a word w ...
application/pdf
PDF (228kB) 
Chen, Feng; Serbanuta, Traian Florin; Rosu, Grigore (200710)Predictive runtime analysis has been proposed to improve the effectiveness of concurrent program analysis and testing. Observing an execution, predictive runtime analysis extracts causality which is then used as the model ...
application/pdf
PDF (283kB) 
Chen, Feng; Jin, Dongyun; Meredith, Patrick O'Neil; Rosu, Grigore (200809)Efficient monitoring of parametric properties, in spite of increasingly growing interest thanks to applications such as testing and security, imposes a highly nontrivial challenge on monitoring approaches due to the ...
application/pdf
PDF (202kB) 
Chen, Feng; Jin, Dongyun; Meredith, Patrick O'Neil; Rosu, Grigore (200809)Efficient monitoring of parametric properties, in spite of increasingly growing interest thanks to applications such as testing and security, imposes a highly nontrivial challenge on monitoring approaches due to the ...
application/pdf
PDF (202kB) 
Chen, Feng; Meredith, Patrick O'Neil; Jin, Dongyun; Rosu, Grigore (20090512)
application/pdf
PDF (3MB) 
Meredith, Patrick O'Neil; Jin, Dongyun; Chen, Feng; Rosu, Grigore (200804)Recent developments in runtime verification and monitoring show that parametric regular and temporal logic specifications can be efficiently monitored against large programs. However, these logics reduce to ordinary finite ...
application/pdf
PDF (274kB) 
d'Amorim, Marcelo; Rosu, Grigore (200503)We present a technique for generating efficient monitors for Omegaregularlanguages. We show how Buchi automata can be reduced in size and transformed into special, statistically optimal nondeterministic finite state ...
application/pdf
PDF (284kB) 
Meredith, Patrick; Rosu, Grigore (20120401)Early efforts in runtime verification and monitoring show that parametric regular and temporal logic specifications can be monitored efficiently. These approaches, however, have limited expressiveness, since their ...
application/pdf
PDF (349kB)
Now showing items 120 of 94