The degree-constrained minimum spanning tree (DCMST) problem is the problem of finding the minimum cost spanning tree in an edge weighted complete graph such that each vertex in the spanning tree has degree ≤dfor somed≥ 2. The DCMST problem is known to be NP-hard. This paper presents an ant-based algorithm to find low cost degree-constrained spanning trees (DCST). The algorithm employs a set of ants which traverse the graph and identify a set of candidate edges, from which a DCST is constructed. Local optimization algorithms are then used to further improve the DCST. Extensive experiments using 612 problem instances show many improvements over existing algorithms.

Automated theorem proving techniques such as Satisfiability Modulo Theory (SMT) solvers have seen significant advances in the past several years. These advancements, coupled with vast hardware improvements, have drastic impact on, for example, program verification techniques and tools. The general availability of robust general purpose solvers have reduced a significant engineering overhead when designing and developing program verifiers. However, most solver implementations are designed to be used as a black box, and due to their aim as general purpose solvers, they often miss optimization opportunities that can be done by leveraging domain-specific knowledge.

Recent work has demonstrated that symbolic execution techniques can serve as a basis for formal analysis capable of automatically checking heap-manipulating software components against strong interface specifications. In this paper, we present an enhancement to existing symbolic execution algorithms for object-oriented programs that significantly improves upon the algorithms currently implemented in Bogor/Kiasan and JPF. To motivate and justify the new strategy for handling heap data in our enhanced approach, we present a significant empirical study of the performance of related algorithms and an interesting case counting analysis of the heap shapes that can appear in several widely used Java data structure packages.

Best program practices in software engineering emphasize software components that are loosely coupled and can be independently developed by different vendors. While these approaches improve the process of software development, however, they present a number of challenges involving reasoning about the correctness of individual components as well as their integration. Design-by-contract reasoning offers a promising approach to reason about software components by requiring software contracts that describe the behaviors of the components. This allows one to focus at satisfying the contract of each component, i.e., it allows compositional reasoning. In this paper, we present Kiasan, a technique that combines symbolic execution, model checking, theorem proving, and constraint solving to support design-by-contract reasoning of object-oriented software. There are a number of interesting tradeoffs between Kiasan other approaches such as ESC/Java. While checking in Kiasan is sometime more expensive, Kiasan can check much stronger behavioral properties of object-oriented software including properties/software that makes extensive use of heap-allocated data. In addition, Kiasan naturally generates counter examples, visualization of code effects, and JUnit test cases that are driven by code and user-supplied specifications. We present Kiasan and describe how it is implemented on top of the Bogor framework. Furthermore, we present a case study in which Kiasan is applied to a variety of examples and we discuss insights gained from our experience.

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. Kiasan is able to check strong heap properties, and it is fully automatic and flexible in terms of its cost and the guarantees it provides. It allows a user-adjustable mixed compositional/non-compositional reasoning and naturally produces error traces as fault evidence. We implemented Kiasan using the Bogor model checking framework and observed that its performance is comparable to ESC/Java on similar scales of problems and behavioral coverage, while providing the ability to check much stronger specifications

The use of component models such as Enterprise Java Beans and the CORBA Component Model (CCM) in application development is expanding rapidly. Even in real-time safety/mission-critical domains, component-based development is beginning to take hold as a mechanism for incorporating non-functional aspects such as real-time, quality-of-service, and distribution. To form an effective basis for development of such systems, we believe that support for reasoning about correctness properties of component-based designs is essential. In this paper, we present Cadena - an integrated environment for building and modeling CCM systems. Cadena provides facilities for defining component types using CCM IDL, specifying dependency information and transition System semantics for these types, assembling systems from CCM components, visualizing various dependence relationships between components, specifying and verifying correctness properties of models of CCM systems derived from CCM IDL, component assembly information, and Cadena specifications, and producing CORBA stubs and skeletons implemented in Java. We are applying Cadena to avionics applications built using Boeing's Bold Stroke framework.

Concurrency is used in modern software systems as a means of addressing performance, availability, and reliability requirements. The collaboration of multiple independently executing components is fundamental to meeting such requirements and such collaboration is realized by synchronizing component execution.Using current technologies developers are faced with a tension between correct synchronization and performance. Developers can be confident when simple forms of synchronization are used, for example, locking all accesses to shared data. Unfortunately, such simple approaches can result in significant run-time overhead, and, in fact, there are many cases in which such simple approaches cannot implement required synchronization policies. Implementing more sophisticated (and less constraining) synchronization policies may improve run-time performance and satisfy synchronization requirements, but fundamental difficulties in reasoning about concurrency make it difficult to assess their correctness.This paper describes an approach to automatically synthesizing complex synchronization implementations from formal high-level specifications. Moreover, the generated coded is designed to be processed easily by software model-checking tools such as Bandera. This enables the generated synchronization solutions to be verified for important system correctness properties. We believe this is an effective approach because the tool-support provided makes it simple to use, it has a solid semantic foundation, it is language independent, and we have demonstrated that it is powerful enough to solve numerous challenging synchronization problems.