An increasing number of applications in verification and security rely on or could benefit from automatic solvers that can check the satisfiability of constraints over a rich set of data types that includes character strings. Unfortunately, most string solvers today are standalone tools that can reason only about some fragment of the theory of strings and regular expressions, sometimes with strong restrictions on the expressiveness of their input language (such as, length bounds on all string variables). These specialized solvers reduce string problems to satisfiability problems over specific data types, such as bit vectors, or to automata decision problems. On the other side, despite their power and success as back-end reasoning engines, general-purpose Satisfiability Modulo Theories (SMT) solvers so far have provided minimal or no native support for string reasoning. This thesis presents a deductive calculus describing a new algebraic approach that allows solving constraints over the theory of unbounded strings and regular expressions natively, without reduction to other problems. We provide proofs of refutation soundness and solution soundness of our calculus, and solution completeness under a fair proof strategy. Moreover, we show that our calculus is a decision procedure for the theory of regular language membership with length constraints. We have implemented our calculus as a string solver for the theory of (unbounded) strings with concatenation, length, and membership in regular languages, and incorporated it into the SMT solver CVC4 to expand its already large set of built-in theories. This work makes CVC4 the first SMT solver that is able to accept and process a rich set of mixed constraints over strings, integers, reals, arrays and other data types. In addition, our initial experimental results show that, over string problems, CVC4 is highly competitive with specialized string solvers with a comparable input language. We believe that the approach we described in this thesis provides a new idea for string-based formal methods.

Owing to advancements in component re-use technology, component-based software development (CBSD) has come a long way in developing complex commercial software systems while reducing software development time and cost. However, assembling distributed resource-constrained and safety-critical systems using current assembly techniques is a challenge. Within complex systems when there are numerous ways to assemble the components unless the software architecture clearly defines how the components should be composed, determining the correct assembly that satisfies the system assembly constraints is difficult. Component technologies like CORBA and .NET do a very good job of integrating components, but they do not automate component assembly; it is the system developer's responsibility to ensure thatthe components are assembled correctly. In this thesis, we first define a component-based system assembly (CBSA) technique called "Constrained Component Assembly Technique" (CCAT), which is useful when the system has complex assembly constraints and the system architecture specifies component composition as assembly constraints. The technique poses the question: Does there exist a way of assembling the components that satisfies all the connection, performance, reliability, and safety constraints of the system, while optimizing the objective constraint? To implement CCAT, we present a powerful framework called "CoBaSA". The CoBaSA framework includes an expressive language for declaratively describing component functional and extra-functional properties, component interfaces, system-level and component-level connection, performance, reliability, safety, and optimization constraints. To perform CBSA, we first write a program (in the CoBaSA language) describing the CBSA specifications and constraints, and then an interpreter translates the CBSA program into a satisfiability and optimization problem. Solving the generated satisfiability and optimization problem is equivalent to answering the question posed by CCAT. If a satisfiable solution is found, we deduce that the system can be assembled without violating any constraints. Since CCAT and CoBaSA provide a mechanism for assembling systems that have complex assembly constraints, they can be utilized in several industries like the avionics industry. We demonstrate the merits of CoBaSA by assembling an actual avionic system that could be used on-board a Boeing aircraft. The empirical evaluation shows that our approach is promising and can scale to handle complex industrial problems.

In recent years many people have built Personal Assistant Agents, Information Agents and the like, and have simply added them to the operating system as auxiliary applications, without regard to architecture. This thesis argues that an agent architecture, one designed as a sophisticated representation of an individual user, should be embedded deep in the device system software, with at least equal status to the GUI – the graphical user interface. A sophisticated model of the user is then built, drawing upon contemporary Analytical Psychology – the Psychology of Subselves. The Shadowboard Agent architecture is then built upon that user model, drawing both structural and computational implications from the underlying psychology. An XML DTD file named Shadowboard.dtd is declared as a practical manifestation of the semantics of Shadowboard. An implementation of the Shadowboard system is mapped out, via a planned conversion of two existing integrated systems: SlimWinX, an event-driven GUI system; and XSpaces, an object-oriented tuplespace system with Blackboard-like features. The decision making mechanism passes logic terms and contraints between the various sub-agent components (some of which take on the role of Constraint Solvers), giving this agent system some characteristics of a Generalised Constraint Solver. A Shadowboard agent (built using the system) consists of a central controlling autonomous agent named the Aware Ego Agent, and any number of sub-agents, which collectively form an integrated but singular whole agent modelled on the user called the Digital Self. One such whole-agent is defined in a file named DigitalSelf.xml – which conforms to the schema in Shadowboard.dtd - which offers a comprehensive and generic representation of a user’s stance in a 24x7 network, in particular - the Internet. Numerous types of Shadowboard sub-agents are declared.

The modal satisfiability problem has to date been solved using either a specifically designed algorithm, or by translating the modal logic formula into a different class of problem, such as a first-order logic, a propositional satisfiability problem or a constraint satisfaction problem. These approaches and the solvers developed to support them are surveyed and a synthesis thereof is presented. The translation of a modal K formula into a constraint satisfaction problem, as developed by Brand et al. [18], is further enhanced. The modal formula, which must be in conjunctive normal form, is translated into layered propositional formulae. Each of these layers is translated into a constraint satisfaction problem and solved using the constraint solver ECLiPSe. I extend this translation to deal with reflexive and transitive accessibility relations, thereby providing for the modal logics KT and S4. Two of the difficulties that arise when these accessibility relations are added are that the resultant formula increases considerably in complexity, and that it is no longer in conjunctive normal form (CNF). I eliminate the need for the conversion of the formula to CNF and deal instead with formulae that are in negation normal form (NNF). I apply a number of enhancements to the formula at each modal layer before it is translated into a constraint satisfaction problem. These include extensive simplification, the assignment of a single value to propositional variables that occur only positively or only negatively, and caching the status of the formula at each node of the search tree. All of these significantly prune the search space. The final results I achieve compare favorably with those obtained by other solvers. / Computing / M.Sc. (Computer Science)

The modal satisfiability problem has to date been solved using either a specifically designed algorithm, or by translating the modal logic formula into a different class of problem, such as a first-order logic, a propositional satisfiability problem or a constraint satisfaction problem. These approaches and the solvers developed to support them are surveyed and a synthesis thereof is presented. The translation of a modal K formula into a constraint satisfaction problem, as developed by Brand et al. [18], is further enhanced. The modal formula, which must be in conjunctive normal form, is translated into layered propositional formulae. Each of these layers is translated into a constraint satisfaction problem and solved using the constraint solver ECLiPSe. I extend this translation to deal with reflexive and transitive accessibility relations, thereby providing for the modal logics KT and S4. Two of the difficulties that arise when these accessibility relations are added are that the resultant formula increases considerably in complexity, and that it is no longer in conjunctive normal form (CNF). I eliminate the need for the conversion of the formula to CNF and deal instead with formulae that are in negation normal form (NNF). I apply a number of enhancements to the formula at each modal layer before it is translated into a constraint satisfaction problem. These include extensive simplification, the assignment of a single value to propositional variables that occur only positively or only negatively, and caching the status of the formula at each node of the search tree. All of these significantly prune the search space. The final results I achieve compare favorably with those obtained by other solvers. / Computing / M.Sc. (Computer Science)