Nikhil Naik is a PhD graduate from the Ming Hsieh Department of Electrical and Computer Engineering, University of Southern California. He worked under the supervision of Prof. Pierluigi Nuzzo. He received his Bachelor of Technology (Hons.) Degree in Instrumentation Engineering from the Department of Electrical Engineering, Indian Institute of Technology, Kharagpur in 2018, and an MS degree in Electrical and Computer Engineering from the University of Southern California in 2020. He is a recipient of the Annenberg Fellowship from USC, the DAC Young Fellowship Award from the Design Automation Conference in 2021, and the JPL Graduate Fellowship (JPLGF) from the NASA Jet Propulsion Laboratory in 2023. He is currently based in East Hartford, Connecticut, working as a senior engineer at the industrial research laboratory of a major defense conglomerate in the USA.

Designing complex systems such as space rovers is typically a hierarchical process. Beginning with a conceptual model of the system, these processes culminate in the realization of each system component, followed by component integration and system performance evaluation. Owing to this layered heterogeneity, verifying correctness, completeness, and inter-layer traceability for safety and mission assurance is challenging. Further, existing manual verification methods may be intractable in the emerging paradigm of autonomous cyber-physical systems.

We present formal approaches to tackle this challenge of assured autonomy, namely, developing scalable design and verification algorithms to provide sound performance guarantees. Our work leverages assume-guarantee contracts, a specification paradigm founded on model-based design. Contracts capture the scope of operation of each component in a system, specifying how a component is expected to operate (guarantees), subject to its functional context (assumptions). Contracts facilitate scalability through a rigorous algebra, which supports compositional design and verification methods. We model requirement hierarchies with a graph of contracts, which we term heterogeneous hierarchical contract networks, through which traceability validation can be performed algorithmically. We introduce contract embeddings to rigorously map contracts between different abstraction layers and use them for automatically decomposing system-level specifications into component specifications. We show how contract embeddings can support compositional design for layered control architectures, in which the coordination of different objectives, such as high-level planning and low-level safe control, is essential. Then, we discuss contract-based specification frameworks for deep neural networks, which enable verification of multiple robustness properties on neural networks and scalable verification of closed-loop neural network-controlled systems. We conclude by summarizing ongoing work and outlining future directions toward resilient design of autonomous systems.

Dr. Sabyasachi Basu is a postdoctoral researcher at Microsoft Research India, where he works with the vector search team (DiskANN) on problems in quantization and retrieval. He earned his PhD in Computer Science from the University of California, Santa Cruz, where he worked with C. Seshadhri on sublinear algorithms and graph decompositions. Previously, he completed his undergraduate studies in Mathematics at IISc Bangalore. His research interests include using theoretical insights to design algorithms for real-world data and exploring theoretical questions arising from empirical observations.

Decompositions of large-scale networks are central to many applications in graph mining, network science, and algorithm design. Over several decades, a rich body of work has developed techniques to partition networks with various different objectives. However, a noticeable gap persists between methods with strong theoretical guarantees and those that perform well in practice. Practical algorithms often lack provable guarantees, while theoretically sound methods are rarely straightforward to implement and scale poorly.

This talk presents a suite of techniques aimed at bridging this gap, focusing on dense subgraph decomposition — a fundamental problem with numerous real-world applications and a close relation to community detection. We introduce fast, theoretically grounded algorithms that perform efficiently on large datasets, along with new objectives and frameworks that capture structural properties of real-world networks. If time permits, Dr. Basu will also discuss challenges and successes in developing similar algorithms for overlapping clusters.