The synthesis of logical controllers that guarantee desired specifications is a central problem in the design of cyber-physical systems (CPS). In practice, such guarantees rely on assumptions about how the controller interacts with its environment. These assumptions restrict environment behavior to make synthesis feasible, but in existing approaches they are often overly restrictive, leading to conservative designs and limiting the range of behaviors that systems can safely accommodate.

This thesis rethinks the role of assumptions in logical controller synthesis by emphasizing their \emph{permissiveness}---the ability to capture a wide range of admissible environment behaviors. We study permissive assumptions in two key settings: (a) interactions among multiple discrete components in distributed systems, and (b) interactions between high-level logical controllers and low-level physical dynamics in hybrid systems. In both settings, we develop theoretical and algorithmic foundations for computing and exploiting permissive assumptions to enable new design paradigms for logical controller synthesis.

For distributed systems, we define permissiveness as capturing all cooperative behaviors of other components that enable a controller to satisfy its specification. We present an algorithm for computing such assumptions in monolithic systems and extend it to distributed systems via a negotiation-based framework that iteratively constructs permissive assume-guarantee contracts for each component. These contracts enable decentralized synthesis and are applied to human-robot interaction, allowing robots to cooperate with humans whenever possible and request cooperation only when necessary.

For hybrid systems, we utilize permissive assumptions on the plant model---the abstract representation of physical dynamics---to address three key challenges. To enable seamless adaptation of controllers to changing logical contexts, i.e., changes in high-level goals or tasks, we introduce a novel synthesis framework that utilizes \emph{persistent live groups}, a class of assumptions capturing liveness properties of continuous dynamics. To improve scalability to large or uncertain plant models, we develop \emph{universal controllers} where decisions are conditioned on branching-time assumptions called \emph{prophecies}, which are learned from representative models and efficiently verified at runtime on unseen plant models. Finally, to enhance robustness under uncertainty or partial violations of assumptions on the plant model, we introduce a robust semantics for branching-time temporal logics, enabling formal reasoning about controller behavior under such violations.

Overall, this work enables correctness-by-construction synthesis while avoiding unnecessary conservatism, resulting in CPS that are more robust, scalable, and responsive.

Floating-point numbers often represent real numbers in computer systems. They are applicable in many domains, including embedded systems, machine learning, and scientific computing. Despite their widespread use, they pose some difficulties. Floating-point numbers and operations typically suffer from roundoff errors, making computations over floating-points inaccurate with respect to a real-valued specification. Moreover, the IEEE 754 floating-point standard, a fundamental element in formalizing floating-point arithmetic for today’s computers, presents additional challenges due to special values and resulting unintuitive behaviors. This thesis has three main contributions that address existing gaps in automated reasoning about floating-point arithmetic, making it easier for developers and researchers to understand, verify, and trust the floating-point computations in their programs. First, we introduce the first floating-point support in a deductive verifier for the Java programming language. Our support in the KeY verifier automatically handles floating-point arithmetic and transcendental functions. We achieve this with a combination of delegation to external SMT solvers on one hand, and rule-based reasoning within KeY on the other, exploiting the complementary strengths of both approaches. As a result, this approach can prove functional floating-point properties for realistic programs. Second, inspired by KeY’s treatment of method calls and the need for a scalable roundoff error analysis, we present the first modular optimization-based roundoff error analysis for non-recursive procedural floating-point programs. Our key idea is to achieve modularity while maintaining reasonable accuracy by automatically computing procedure summaries that are a function of the input parameters. Technically, we extend an existing optimization-based roundoff error analysis and show how to effectively use first-order Taylor approximations to compute precise procedure summaries, and how to integrate those to obtain end-to-end roundoff error bounds. Third, our experience using SMT solvers to discharge KeY’s floating-point verification conditions revealed unexpected performance behavior, motivating a systematic study of floating-point reasoning in SMT solvers. We propose a metamorphic testing approach that uses semantics-preserving rewrite rules, focusing on floating-point special values, to uncover unexpected performance behavior in SMT solvers’ handling of floating-point formulas, such as an increase in solving time when the SMT queries are simplified. Using real-world test inputs, our approach can identify such performance bugs for every SMT solver tested.