The need to solve non-linear arithmetic constraints presents a major obstacle to the automatic verification of smart contracts. In this case study we focus on the two overapproximation techniques used by the industry verification tool Certora Prover: overapproximation of non-linear integer arithmetic using linear integer arithmetic and using non-linear real arithmetic. We compare the performance of contemporary SMT solvers on verification conditions produced by the Certora Prover using these two approximations against the natural non-linear integer arithmetic encoding. Our evaluation shows that the use of the overapproximation methods leads to solving a significant number of new problems.

Microsoft's Static Driver Verifier (SDV) pioneered the use of software model checking for ensuring that device drivers correctly use operating system (OS) APIs.However, the verification methodology has been difficult to extend in order to support either (a) new classes of drivers for which SDV does not already have a harness and stubs, or (b) memory-corruption properties.Any attempt to apply SDV out-of-the-box results in either false alarms due to the lack of environment modeling, or scalability issues when finding deeply nested bugs in the presence of a very large number of memory accesses.In this paper, we describe our experience designing and shipping a new class of checks known as angelic checks through SDV with the aid of angelic verification (AV) [1] technology, over a period of 4 years.AV pairs a precise inter-procedural assertion checker with automatic inference of likely specifications for the environment.AV helps compensate for the lack of environment modeling and regains scalability by making it possible to find deeply nested bugs, even for complex memorycorruption properties.These new rules have together found over a hundred confirmed defects during internal deployment at Microsoft, including several previously unknown high-impact potential security vulnerabilities.AV considerably increases the reach of SDV, both in terms of drivers as well as rules that it can support effectively.

Abstract Ultimate Taipan is a software model checker that combines trace abstraction with abstract interpretation on path programs. In this year’s version, we replaced our abstract interpretation engine and now use a combination of multiple abstraction functions, fixpoint computation, algebraic program analysis, and SMT solving. Our new approach will allow us to integrate new techniques more easily.

Ever since the seminal work on SLAM and BLAST, software model checking with counterexample-guided abstraction refinement (CEGAR) has been an active topic of research. The crucial procedure here is to analyze a sequence of program statements (the counterexample) to find building blocks for the overall proof of the program. We can distinguish two approaches (which we name Craig and Newton) to implement the procedure. The historically first approach, Newton (named after the tool from the SLAM toolkit), is based on symbolic execution. The second approach, Craig, is based on Craig interpolation. It was widely believed that Craig is substantially more effective than Newton. In fact, 12 out of the 15 CEGAR-based tools in SV-COMP are based on Craig. Advances in software model checkers based on Craig, however, can go only lockstep with advances in SMT solvers with Craig interpolation. It may be time to revisit Newton and ask whether Newton can be as effective as Craig. We have implemented a total of 11 variants of Craig and Newton in two different state-of-the-art software model checking tools and present the outcome of our experimental comparison.