Browse Dept. of Computer Science by Author "d'Amorim, Marcelo"

  • Automatic and Precise Dimensional Analysis 
    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)
  • Delta Execution for Efficient State-Space Exploration of Object-Oriented Programs 
    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)
  • Efficient Explicit -State Model Checking for Programs With Dynamically Allocated Data 
    d'Amorim, Marcelo (2007)
    We implemented Delta Execution in two model checkers, JPF (Java PathFinder) and BOX (Bounded Object eXploration) to evaluate the effectiveness of this technique in model checkers with different designs. The results show ...

    application/pdf

    application/pdfPDF (4MB)Restricted to U of Illinois
  • Efficient Explicit-State Model Checking for Programs with Dynamically Allocated Data 
    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)
  • Efficient Monitoring of ω-languages 
    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)
  • An Equational Specification for the Scheme Language 
    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)
  • Monitoring-Oriented Programming: A Tool-Supported Methodology for Higher Quality Object-Oriented Software 
    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)
  • Optimized Execution of Deterministic Blocks in Java PathFinder 
    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)
  • Verification of Simulation Models of Network Protocols Using State Space Exploration and Protocol-Specific Properties 
    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)