Automating Elevator Design with Satisfiability Modulo Theories Automating the design of elevator systems poses interesting challenges when it comes to deal with configuration constraints and to express qualityofdesign targets that must also comply to specific norms and regulations. Our automated elevator design tool LIFTCREATE is based on an AI engine featuring specialpurpose heuristic techniques which are successful in handling complex realworld designs, but are lacking flexibility and thus are difficult to extend to, e.g., different classes of systems or different norms and regulations. In this paper we describe the development of a replacement engine for L IFTCREATE which seeks to overcome the limitations of the current one. The new approach is based on satisfiability modulo theories (SMT) with theories of cost. We describe encodings to solve choice and placement of critical components in the elevator, and we experiment with our encodings using a stateoftheart SMT solver. Our experiments show that the SMTbased approach is competitive with respect to the heuristicbased one, both in terms of efficiency and in terms of design quality.

Synthesizing Mutable Configurations: Setting up Systems for Success Numerous devices, from network switches and servers to industrial control systems, can be unreliable if they are not configured properly. Even if a deviceu0027s implementation has been proven correct, it must still be configured to meet the specific functional and security requirements of its stakeholders. However, manual configuration remains labor intensive and errorprone even for experts. Automated configuration synthesis presents a promising way forward. Unfortunately, as we show, existing counterexampleguided algorithms can perform poorly if the system model allows configuration changes during execution. Yet disallowing such changes can hide significant problems, such as privilege escalation. We present a new synthesis algorithm that exploits structure inherent in statemachine models where the system configuration changes. We implement it using the Kodkod relational model finder, and show that it favorably solves a number of configurationsynthesis tasks.