Browse by Author "Rosu, Grigore"

  • d'Amorim, Marcelo; Hills, Mark; Chen, Feng; Rosu, Grigore (2005-12)
    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 ...
    untranslated PDF (244KB)
  • Popescu, Andrei; Rosu, Grigore (2005-05)
    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 ...
    untranslated PDF (332KB)
  • Rosu, Grigore; Stefanescu, Andrei (2012-04)
    This paper presents a verification framework that is parametric in a (trusted) operational semantics of some programming language. The underlying proof system is language-independent and consists of eight proof rules. ...
    untranslated PDF (343KB)
  • Rosu, Grigore; Stefanescu, Andrei (2012-08)
    This paper presents a verification framework that is parametric in a (trusted) operational semantics of some programming language. The underlying proof system is language-independent and consists of eight proof rules. The ...
    untranslated PDF (346KB)
  • Lucanu, Dorel; Rosu, Grigore (2009-02)
    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 ...
    untranslated PDF (260KB)
  • Rosu, Grigore; Lucanu, Dorel (2009-02)
    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 ...
    untranslated PDF (223KB)
  • Rosu, Grigore; Lucanu, Dorel (2009-02)
    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 ...
    untranslated PDF (223KB)
  • Serbanuta, Traian Florin; Rosu, Grigore (2006-02)
    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 ...
    untranslated PDF (330KB)
  • Rosu, Grigore (2003-12)
    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 ...
    untranslated PDF (2MB)
  • Ellison, Chucky; Rosu, Grigore (2012-04-27)
    This paper investigates undefined behavior in C and offers a few simple techniques for operationally specifying such behavior formally. A semantics-based undefinedness checker for C is developed using these techniques, as ...
    untranslated PDF (257KB)
  • Sen, Koushik; Rosu, Grigore; Agha, Gul A. (2004-12)
    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 ...
    untranslated PDF (208KB)
  • Rosu, Grigore (2005-08)
    By adding the complement operator (\neg), extended regular expressions ({\ERE}) can encode regular languages non-elementarily more succinctly than regular expressions. The {\ERE} membership problem asks whether a word w ...
    untranslated PDF (228KB)
  • Chen, Feng; Serbanuta, Traian Florin; Rosu, Grigore (2007-10)
    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 ...
    untranslated PDF (283KB)
  • Chen, Feng; Jin, Dongyun; Meredith, Patrick O'Neil; Rosu, Grigore (2008-09)
    Efficient monitoring of parametric properties, in spite of increasingly growing interest thanks to applications such as testing and security, imposes a highly non-trivial challenge on monitoring approaches due to the ...
    untranslated PDF (202KB)
  • Chen, Feng; Meredith, Patrick O'Neil; Jin, Dongyun; Rosu, Grigore (2009-05-12)
    untranslated PDF (3MB)
  • Chen, Feng; Jin, Dongyun; Meredith, Patrick O'Neil; Rosu, Grigore (2008-09)
    Efficient monitoring of parametric properties, in spite of increasingly growing interest thanks to applications such as testing and security, imposes a highly non-trivial challenge on monitoring approaches due to the ...
    untranslated PDF (202KB)
  • Meredith, Patrick O'Neil; Jin, Dongyun; Chen, Feng; Rosu, Grigore (2008-04)
    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 ...
    untranslated PDF (274KB)
  • d'Amorim, Marcelo; Rosu, Grigore (2005-03)
    We present a technique for generating efficient monitors for Omega-regular-languages. We show how Buchi automata can be reduced in size and transformed into special, statistically optimal nondeterministic finite state ...
    untranslated PDF (284KB)
  • Meredith, Patrick; Rosu, Grigore (2012-04-01)
    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 ...
    untranslated PDF (349KB)
  • Luo, Qingzhou; Rosu, Grigore (2013-03-26)
    Multithreaded programs are hard to develop and test. In order for programs to avoid unexpected concurrent behaviours at runtime, for example data-races, synchronization mechanisms are typically used to enforce a safe subset ...
    untranslated PDF (523KB)