Browse by Author "d'Amorim, Marcelo"

  • 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)
  • d'Amorim, Marcelo; Lauterburg, Steven; Marinov, Darko (2007-05)
    State-space exploration is the essence of model checking and an increasingly popular approach for automating test generation. A key issue in exploration of object-oriented programs is handling the program state, in particular ...

    application/pdf

    application/pdfPDF (300Kb)
  • d'Amorim, Marcelo (2007-08)
    Despite the technological advances in languages and tools to support program development, programmers still deliver software with lots of errors. Software testing has been the dominant approach in industry to improve the ...

    application/pdf

    application/pdfPDF (656Kb)
  • 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)
  • d'Amorim, Marcelo; Rosu, Grigore (2005-04)
    This work describes the formal semantics of Scheme (Based on the publicly available report R5RS) as an equational theory in the Maude rewriting system. The semantics is based on continuations and is highly modular. We ...

    application/pdf

    application/pdfPDF (168Kb)
  • Chen, Feng; d'Amorim, Marcelo; Rosu, Grigore (2004-03)
    This paper presents a tool-supported methodological paradigm for object-oriented software development, called monitoring-oriented programming and abbreviated MOP, in which runtime monitoring is a basic software design ...

    application/pdf

    application/pdfPDF (462Kb)
  • d'Amorim, Marcelo; Sobeih, Ahmed A.; Marinov, Darko (2006-06)
    Java PathFinder (JPF) is an explicit-state model checker for Java programs. It explores all executions that a given program can have due to different thread interleavings and nondeterministic choices. JPF implements a ...

    application/pdf

    application/pdfPDF (176Kb)
  • Sobeih, Ahmed A.; d'Amorim, Marcelo; Viswanathan, Mahesh; Marinov, Darko; Hou, Jennifer C. (2007-08)
    Verification and Validation (V&V) is a critically important phase in the development life cycle of a simulation model. In the context of network simulation, traditional network simulators perform well in using a simulation ...

    application/pdf

    application/pdfPDF (298Kb)