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

Moving Fast with Software Verification

Moving Fast with Software Verification - Calcagno et al. 2015 This is a story of transporting ideas from recent theoretical research in reasoning about programs into the fast-moving engineering culture of Facebook. The context is that most of the authors landed at Facebook in September of 2013, when we brought the INFER static analyser with … Continue reading Moving Fast with Software Verification

IronFleet: Proving Practical Distributed Systems Correct

IronFleet: Proving Practical Distributed Systems Correct - Hawblitzel et al. (Microsoft Research) 2015 Every so often a paper comes along that makes you re-evaluate your world view. I happily would have told you that full formal verification of non-trivial systems (especially distributed systems) in a practical manner (i.e. something you could consider using for real … Continue reading IronFleet: Proving Practical Distributed Systems Correct

SAMC: Semantic-aware model checking for fast discovery of deep bugs in cloud systems

SAMC: Semantic-aware model checking for fast discovery of deep bugs in cloud systems - Leesatapornwongsa et al. 2014 This is the second of three papers we'll be looking at this week on the theme of verifying correctness of, and catching bugs in, distributed systems. Yesterday we saw the Statecall Policy Language and associated tool chain … Continue reading SAMC: Semantic-aware model checking for fast discovery of deep bugs in cloud systems