Research Projects

Automated synthesis has long been essential in generating complex systems—such as functions, programs, or circuits—that meet specified requirements. Traditional synthesis techniques either produce a rigorously verified system that satisfies all constraints or, if even one constraint remains unmet, fail to produce a system at all. While these methods achieve a high level of trustworthiness, this rigid ``all-or-nothing" approach significantly limits the broader adoption of synthesis methods in industry and complex applications. This proposal aims to bridge the gap between trustworthiness and scalability by proposing a novel approach that relaxes the "all-or-nothing" framework by categorizing constraints into two types: (i) essential constraints that require strict guarantees to ensure trustworthiness, and (ii) soft constraints, where it is acceptable to satisfy them as much as possible without absolute guarantees. The motivation behind exploring synthesis with graded constraints stems primarily from the increasing demand for synthesis frameworks that effectively balance essential (hard) constraints, such as policy and safety requirements, with performance-driven criteria. This need is particularly pronounced in the context of data-driven AI models, where optimizing for criteria such as accuracy on training data must coexist with adherence to strict regulatory and ethical policies. The proposed graded-constraint approach thus enables synthesized systems to perform optimally while still adhering to essential trustworthiness requirements. We aim to design a domain-agnostic approach, enhancing the versatility of synthesis in various real-world applications.