Patrick Redmond

I am a PhD student in the Languages, Systems, and Data Lab at the University of California Santa Cruz advised by Lindsey Kuper.

My research is in solver aided verification of distributed systems. Solvers can bring software verification to industry, where rapidly changing production systems are difficult to verify with traditional manual proof-writing techniques.

I have several years of industry experience conceptualizing, developing, and deploying high-availability distributed-systems and machine prediction at scale for Twitch (Amazon), Prismatic (defunct), and Vlingo (Nuance).

Here are some highlights from my CV:

Research

• Verifying CBCAST (draft; code) – I am working to verify a causal delivery algorithm using Liquid Haskell with collaborators at UCSC and IMDEA.

• Verifying CRDTs (OOPSLA20; code) – I wrote a server and model applications to demonstrate verified CRDTs for work with collaborators at UCSC, UMD, and IMDEA.

• Tracking Larva (Science Signalling 10, no. 477; code) – I wrote a deterministic point tracker for a larval-crawling autism therapy drug assay for work with researchers at UCSF.

Teaching

• CSE138, Distributed Systems – At UCSC I was the TA for distributed systems in Spring-2021 & Fall-2021. I was awarded Best TA Award for Spring-2021.

Industry

• Edge Allocator – At Twitch I replaced the system which allocates video edge servers to content streams. The new system required less hardware and fixed overcommitting of edge servers.
• Service Authorizer – I created a system to provide AWS credentials to all bare-metal servers at Twitch. Folks called it “magic” because it integrated seamlessly with the AWS SDK.

• 
• GitHub: plredmond
• ORCID: 0000-0001-5702-0860
• Scopus Author: 56330150100