Summary. Abstract Execution (AE) is a new program analysis technique for automatically proving second-order properties about programs. It is based on the symbolic execution of abstract programs with second-order symbolic stores. Abrupt completion is analyzed in separate SE branches. AE has been successfully applied to show that almost all statement-based Java refactoring techniques are unsound—unless constrained with suitable preconditions. Assuming these preconditions, we automatically proved the transformations correct. With REFINITY, there is now tool support for using AE for your own problems.
Continue reading “Proving the Correctness of Program Transformations with Abstract Execution and REFINITY”Category: Case Study
Proving Smart Contracts with KeY
With smart contracts, it is really important to get them right at the first try. See how KeY can be used to prove the correctness of Hyperledger Fabric chaincode!
Proving JDK’s Dual Pivot Quicksort Correct
by Bernhard Beckert, Jonas Schiffl, Peter H. Schmitt and Mattias Ulbrich
Sorting is a fundamental functionality in libraries, for which efficiency is crucial. Correctness of the highly optimized implementations is often taken for granted. De Gouw et al. have shown that this certainty is deceptive by revealing a bug in the Java Development Kit (JDK) implementation of TimSort.
We have now formally analysed the other implementation of sorting in the JDK standard library: A highly efficient implementation of a dual pivot quicksort algorithm. We were able to deductively prove that the algorithm implementation is correct. However, a loop invariant which is annotated to the source code does not hold. Continue reading “Proving JDK’s Dual Pivot Quicksort Correct”