3,458 papers · page 139 of 173
This paper presents Kiasan, a bounded technique to reason about open systems based on a path sensitive, relatively sound and complete symbolic execution instead of the usual compositional reasoning through weakest precondition calculation that summarizes all execution paths. Kias…
Automated code generation is an enabling technology for model-based software development and promises many benefits, including higher quality and reduced turn-around times. However, the key to realizing these benefits is generator correctness: nothing is gained from replacing man…
Existing methods and tools supporting product line variability management typically emphasize either the feature or the architecture level. There have been attempts to combine these aspects, but no widely accepted method is available so far. This paper reports ongoing research in…
To improve the productivity of the development process, more and more tools for static software analysis are tightly integrated into the incremental build process of an IDE. If multiple interdependent analyses are used simultaneously, the coordination between the analyses becomes…
The evolution of software engineering methodology, from waterfall to spiral, from spiral to agile, indicates that high concurrency, iterative development and short cycles are key factors for effective software engineering. It is widely accepted that supporting (i.e., formalizing …
Instead of developing user interfaces (UIs) directly, we argue for specifying an interaction design from which UIs can be automatically synthesized. We present an approach to using communicative acts in high-level specification of interaction design, which is implemented and allo…
The aspect-oriented paradigm allows weaving aspects in different join points of a program. Aspects can modify object fields and method control flow, thus possibly introducing subtle and undesired interactions (conflicts) among aspects and objects, which are not easily detectable.…
Verifying specifications is still one of the most important undeveloped research topics in software engineering. It is important because quite a few critical bugs are caused at the level of domains, requirements, and/or designs. It is also important for the cases where no program…
Machine learning provides techniques to monitor system behavior and predict failures from sensor data. However, such algorithms are "scale resistant" $high computational complexity and not parallelizable. The problem then becomes identifying and delivering the relevant subset of …
Domain-specific visual language editors are useful in many areas of software engineering but developing such editors is challenging and time-consuming. We describe an approach to generating a wide range of these graphical editors for use as plug-ins to the Eclipse environment. To…
The testing of database applications poses new challenges for software engineers. In particular, it is difficult to thoroughly test the interactions between an application and its underlying database, which typically occur through dynamically-generated database commands. Because …
Today's complex computational and embedded systems compute complex quantities from complex inputs, with behavior dependent upon the (distributed) state of the system and its environment. Describing the intended behavior of such a system is challenging. The most natural and common…
We propose a new Web browser supporting asynchronous communication with Web server computers like Ajax approach. When users access Web applications on our browser, the users can receive similar benefits from Ajax even if the Web applications do not adopt Ajax approach. The browse…
Large teams of practitioners (developers, testers, etc.) usually work in parallel on the same code base. A major concern when working in parallel is the introduction of integration bugs in the latest shared code. These latent bugs are likely to slow down the project unless they a…
Separation logic holds the promise of supporting scalable formal reasoning for pointer programs. Here we consider proof automation for separation logic. In particular we propose an approach to automating partial correctness proofs for recursive procedures. Our proposal is based u…
Determining the security properties satisfied by software using cryptography is difficult: Security requirements such as secrecy, integrity and authenticity of data are notoriously hard to establish, especially in the context of cryptographic interactions. Nevertheless, little at…
Bug-fixes are widely used for predicting bugs or finding risky parts of software. However, a bug-fix does not contain information about the change that initially introduced a bug. Such bug-introducing changes can help identify important properties of software bugs such as correla…
This paper presents an approach to automate test generation from a formal specification and a set of functional test objectives while taking into account coverage constraints at the specification level. We use existing test generation techniques and tools, our contribution is on …
Tobias is a combinatorial testing tool that was used succesfully on several case studies. Currently, the evolution of the tool goes through a significant redevelopment effort. A first step is the production of an executable specification of the Tobias Test Generator. The goal of …
The need to manually specify temporal properties of software systems is a major barrier to wider adoption of software model checking, because the specification of software temporal properties is a difficult, time-consuming, and error-prone process. To address this problem, we pro…