Browse by Author "d'Amorim, Marcelo"
Now showing items 1-9 of 9
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...