Who? Inigo Incer

What? Formal and Efficient Analysis and Design of Complex Systems 

When? Tuesday, February 06, 2024 @ 11 a.m.

Where? CODA 9th floor Atrium 0920 or virtually on Zoom

Will there be free lunch? YES!

Additional information

Abstract: The task of system design is shared by all engineering disciplines, each coming  

with its own techniques. In spite of their differences in tools, there is large  

intersection in their conceptual approach to design. In this talk, we exploit  

this commonality to take an abstract view of systems and their composition. We  

understand systems and subsystems in terms of their assume-guarantee  

specifications, or contracts.  

Assume-guarantee contracts are formal specifications that state (i) the  

assumptions that a design element makes on its environment and (ii) the  

guarantees it delivers when the environment behaves according to the contract's  

assumptions. Contracts come with a rich algebra that allows us to carry out  

several design-relevant tasks: obtaining system-level specifications from  

component specifications, finding specifications of components that need to be  

added to a design in order to meet an objective, etc. We will introduce the  

algebra of contracts and discuss how the various algebraic operations relate to  

system-design tasks. We will discuss hypercontracts, an extension of  

assume-guarantee reasoning to support the formal analysis of key security and  

robustness properties. We will also discuss the application of this methodology  

and Pacti, a software package that supports system design using contracts, in  

applications ranging from space-mission design to synthetic biology.  

Bio: Inigo Incer is a postdoctoral researcher at Caltech and UC Berkeley. He obtained  

his PhD from UC Berkeley in 2022 under the guidance of Alberto  

Sangiovanni-Vincentelli. He is interested in all aspects of cyber-physical  

systems, emphasizing formal methods and AI that support their compositional  

design and analysis. Before pursuing a PhD, Inigo was an IC designer in Austin.  

His work has been supported by the NSF/ASEE eFellows program and the UC Berkeley  

Chancellor's Fellowship.  

Zoom Link: https://gatech.zoom.us/webinar/register/WN_I_NIDrazS-OFf0VqMOR4Vg