In situations in which developers are not familiar with a system or its documentation is inadequate, the system’s source code becomes the only reliable source of information. Unf...
Vladimir Jakobac, Alexander Egyed, Nenad Medvidovi...
Model-checking is becoming an accepted technique for debugging hardware and software systems. Debugging is based on the “Check / Analyze / Fix” loop: check the system against a...
It is a key activity in CBD to identify high-quality components which have high cohesion and low coupling. However, component clustering is carried out in manual fashion by develop...
Web Services are the basic building blocks of next generation Internet applications, based on dynamic service discovery and composition. Dedicated discovery services will store bot...
Abstract. Coalgebra has in recent years been recognized as the framework of choice for the treatment of reactive systems at an appropriate level of generality. Proofs about the rea...
Abstract. Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast statically proves ...
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rup...
Abstract. The build architecture of legacy C/C++ software systems, groups program files in directories to represent logical components. The interfaces of these components are loos...
Homayoun Dayani-Fard, Yijun Yu, John Mylopoulos, P...