HoTTSQL: Proving query rewrites with univalent SQL semantics

HoTTSQL: Proving query rewrites with univalent SQL semantics Chu et al., PLDI’17 Query rewriting is a vital part of SQL query optimisation, in which rewrite rules are applied to a query to transform it into forms with (hopefully!) a lower execution cost. Clearly when a query is rewritten we still want it to mean the … Continue reading HoTTSQL: Proving query rewrites with univalent SQL semantics

An empirical study on the correctness of formally verified distributed systems

An empirical study on the correctness of formally verified distributed systems Fonseca et al., EuroSys'17 "Is your distributed system bug free?" "I formally verified it!" "Yes, but is your distributed system bug free?" There's a really important discussion running through this paper - what does it take to write bug-free systems software? I have a … Continue reading An empirical study on the correctness of formally verified distributed systems

On formalism in specifications

On formalism in specifications Bertrand Meyer, IEEE Software 1985 Following yesterday’s paper that used formal specification methods to resolve ambiguities and uncover potential vulnerabilities in OAuth 2.0, today’s choice is a 1980’s classic from Bertrand Meyer on the merits of formal specification and what it adds beyond natural language descriptions. With thanks once more to … Continue reading On formalism in specifications

Chapar: Certified Causally Consistent Distributed Key-Value Stores

Chapar: Certified Causally Consistent Distributed Key-Value Stores - Lesani et al. 2016 Another POPL '16 paper today. The Chapar framework provides for modular verification of causal consistency for both causally consistent key-value store implementations and for client programs written to use them. §1 also wins the prize for best use of emojis in a research … Continue reading Chapar: Certified Causally Consistent Distributed Key-Value Stores