The problem of verifying properties of large, networked cyberphysical systems (CPS) is beyond the reach of most computational tools today. Two common "divide-and-conquer" techniques for CPS verification are assume-guarantee contracts from the formal methods literature and input-output properties from the control theory literature. Combining these two approaches, we first introduce the notion of a parametric assume-guarantee contract, which lets one reason about system behavior abstractly in a parameter domain. We next show how a finite gain property can be encoded in this form and provide a generalized small-gain theorem for parametric assume-guarantee contracts. This theorem recovers the classical small gain theorem as a special case and its derivation highlights the connection between assume-guarantee reasoning and small-gain results. This new small-gain theorem applies to behaviors beyond bounded deviation from a nominal point to include a fragment of linear temporal logic with parametrized predicates that can encode safety, recurrence, and liveness properties. Our results are validated with an example which certifies that the interconnection of two freeway segments experiences intermittent congestion.

We address the problem of determining the satisfiability of a Boolean combination of convex constraints over the real numbers, which is common in the context of hybrid system verification and control. We first show that a special type of logic formulas, termed monotone Satisfiability Modulo Convex (SMC) formulas, is the most general class of formulas over Boolean and nonlinear real predicates that reduce to convex programs for any satisfying assignment of the Boolean variables. For this class of formulas, we develop a new satisfiability modulo convex optimization procedure that uses a lazy combination of SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. Our approach can then leverage the efficiency and the formal guarantees of state-of-the-art algorithms in both the Boolean and convex analysis domains. A key step in lazy satisfiability solving is the generation of succinct infeasibility proofs that can support conflict-driven learning and decrease the number of iterations between the SAT and the theory solver. For this purpose, we propose a suite of algorithms that can trade complexity with the minimality of the generated infeasibility certificates. Remarkably, we show that a minimal infeasibility certificate can be generated by simply solving one convex program for a sub-class of SMC formulas, namely ordered positive unate SMC formulas, that have additional monotonicity properties. Perhaps surprisingly, ordered positive unate formulas appear themselves very frequently in a variety of practical applications. By exploiting the properties of monotone SMC formulas, we can then build and demonstrate effective and scalable decision procedures for problems in hybrid system verification and control, including secure state estimation and robotic motion planning.