A Billion SMT Queries a Day (Invited Paper)
Author:
Open Access
- 7 August 2022
- book chapter
- Published by Springer Nature
- p. 3-18
Abstract
Amazon Web Services (AWS) is a cloud computing services provider that has made significant investments in applying formal methods to proving correctness of its internal systems and providing assurance of correctness to their end-users. In this paper, we focus on how we built abstractions and eliminated specifications to scale a verification engine for AWS access policies, Zelkova, to be usable by all AWS users. We present milestones from our journey from a thousand SMT invocations daily to an unprecedented billion SMT calls in a span of five years. In this paper, we talk about how the cloud is enabling application of formal methods, key insights into what made this scale of a billion SMT queries daily possible, and present some open scientific challenges for the formal methods community.Keywords
This publication has 38 references indexed in Scilit:
- PACM SIGPLAN Notices, 2013
- SMT proof checking using a logical frameworkFormal Methods in System Design, 2012
- A decade of software model checking with SLAMCommunications of the ACM, 2011
- HOL Light: An Overview2009
- Explaining abstract counterexamplesACM SIGSOFT Software Engineering Notes, 2004
- Minimization of Counterexamples in SPIN2004
- Automatic predicate abstraction of C programsACM SIGPLAN Notices, 2001
- Algorithm portfoliosArtificial Intelligence, 2001
- An Economics Approach to Hard Computational ProblemsScience, 1997
- The Algorithm Selection Problem1976