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

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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. ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (202Kb)
  • Chen, Feng; Meredith, Patrick O'Neil; Jin, Dongyun; Rosu, Grigore (2009-05-12)

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (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 ...

    application/pdf

    application/pdfPDF (523Kb)