Discover[i]: Component-based Parameterized Reasoning for Distributed Applications
Distributed systems are hard to get right. There have been many notable efforts in formal reasoning for distributed systems: these efforts have focused on language design, automated or semi-automated verification, and, more recently, on automated…
Automated Reasoning of Database Queries
From booking air tickets to analyzing astronomy datasets, database queries are pervasive in people’s work and life. However, reasoning database queries automatically is not easy. It is shown to be undecidable in general. And there…
Reactive Caching for Composed Services
Microsoft @ SPLASH 2018 OOPSLA
Microsoft is excited to be a part of SPLASH 2018 OOPSLA in Boston, Massachusetts November 4 – 9. Microsoft is a gold sponsor and many of our researchers in programming, languages, and software engineering have…
SeeDot: compiler for low-precision machine learning
The emergence of IoT and Machine Learning (ML) has seen an increase in systems that deploy sensors to collect data and analyze the data using ML algorithms in the cloud. However, running the ML classifiers directly…
CHET
CHET is a compiler and runtime that automates many parts of this process for neural network inference tasks. The compiler applies transformations based on a framework of symbolic analysis passes.
TLA+ Specifications of the Consistency Guarantees Provided by Cosmos DB
Microsoft Azure Cosmos DB provides 5 well defined operation consistency properties to the clients: strong consistency, bounded staleness, session consistency, consistent prefix, and eventual consistency. Here we provide client-centric TLA+ specifications of these properties to…