3,458 papers · page 143 of 173
User interfaces are very important for the success of many computer-based applications these days. However, their development takes time, requires experts for user-interface design as well as experienced programmers and is very expensive. This problem becomes even more severe thr…
The use of component-based development (CBD) is growing in the software engineering community and it has been successfully applied in many engineering domains such as office applications and in web-based distributed applications. Recently, the need of CBD is growing also in other…
We introduce a strategy for the verification of relational specifications based on the analysis of monotonicity of variables within formulas. By comparing with the Alloy Analyzer, we show that for a relevant class of problems this technique drastically outperforms analysis of the…
Software is the core constituent of many modern products and services. Many industrial sectors can be considered an "application" of computer science and software engineering, as they increasingly rely on software to provide their features and functionality. For instance, mobile …
We describe an architecture modeling and code generation framework called Bamboo. Using Bamboo, engineers design SCM repository and feature models, and then generate a running SCM system from the models.
Both model and program refactorings are usually proposed in an ad hoc way because it is difficult to prove that they are sound with respect to a formal semantics. In this paper, we propose guidelines on how to rigorously prove model refactorings for Alloy, a formal object-oriente…
Constraint-Based Test data generation (CBT) exploits constraint satisfaction techniques to generate test data able to kill a given mutant or to reach a selected branch in a program. When pointer variables are present in the program, aliasing problems may arise and may lead to the…
Hume is a programming language targeted at safety-critical, resource-bounded systems. Bounded time and space usage is achieved by a clear separation of coordination and computation in the design of the language. However, there is no correctness verification. Such verification is …
Software debugging is the process of locating and correcting faulty code. Prior techniques to locate faulty code either use program analysis techniques such as backward dynamic program slicing or exclusively use delta debugging to analyze the state changes during program executio…
The use of web applications has become increasingly popular in our routine activities, such as reading the news, paying bills, and shopping on-line. As the availability of these services grows, we are witnessing an increase in the number and sophistication of attacks that target …
Debugging is a time-consuming task in software development and maintenance. To accelerate this task, several approaches have been proposed to automate fault localization. In particular, testing based fault localization (TBFL), which utilizes the testing information to localize th…
We consider a formal framework for property verification of web applications using Spin model checker. Some of the web related properties concern all states of the model, while others - only a proper subset of them. To be able to discriminate states of interest in the state space…
Recent work in applying causal modeling (Bayesian networks) to software engineering has resulted in improved decision support systems for software project managers. Once the causal models are built there are commercial tools that can run them. However, data to populate the models…
The term grammar-based software describes software whose input can be specified by a context-free grammar. This grammar may occur explicitly in the software, in the form of an input specification to a parser generator, or implicitly, in the form of a hand-written parser, or other…
Firewalls play a crucial role in network security. Experience has shown that the development of firewall rule sets is complex and error prone. Rule set errors can be costly, by allowing damaging traffic in or by blocking legitimate traffic and causing essential applications to fa…
Building a distributed system from third-party components introduces a set of problems, mainly related to compatibility and communication. Our approach to solve these problems is to build an adaptor which forces the system to exhibit only a set of safe or desired behaviors. By ex…
The high cost of locating faults in programs has motivated the development of techniques that assist in fault localization by automating part of the process of searching for faults. Empirical studies that compare these techniques have reported the relative effectiveness of four e…
Designing and implementing cryptographic protocols is known to be difficult. A lot of research has been devoted to develop formal techniques to analyze abstract designs of cryptographic protocols. Less attention has been paid to the verification of implementation-relevant aspects…
Software for resource constrained embedded devices is often implemented in the Java programming language because the Java compiler and virtual machine provide enhanced safety, portability, and the potential for run-time optimization. It is important to verify that a software appl…
Partial order (p.o.) reduction techniques are a popular and effective approach for tackling state space explosion in the verification of concurrent systems. These techniques generate a reduced search space that could be exponentially smaller than the complete state space. Their m…