26 citations · 74 across the 12 of their papers we have counts for
3 papers · 1 filter
Inferring Formal Properties of Production Key-Value Stores
Edgar Pek, Pranav Garg, Muntasir Raihan Rahman +3
Production distributed systems are challenging to formally verify, in particular when they are based on distributed protocols that are not rigorously described or fully understood.…
A Decidable Fragment of Second Order Logic With Applications to Synthesis
P. Madhusudan, Umang Mathur, Shambwaditya Saha +1
We propose a fragment of many-sorted second order logic called EQSMT and show that checking satisfiability of sentences in this fragment is decidable. EQSMT formulae have an $\exis…
Lagrange's Theorem for Binary Squares
Parthasarathy Madhusudan, Dirk Nowotka, Aayush Rajasekaran +1
We show how to prove theorems in additive number theory using a decision procedure based on finite automata. Among other things, we obtain the following analogue of Lagrange's theo…