6 citations · 14 across the 5 of their papers we have counts for
5 papers
Verifying OpenJDK's LinkedList using KeY
Hans-Dieter A. Hiep, Olaf Maathuis, Jinting Bian +3
As a particular case study of the formal verification of state-of-the-art, real software, we discuss the specification and verification of a corrected version of the implementation…
Reasoning about call-by-value: a missing result in the history of Hoare's logic
Krzysztof R. Apt, Frank S. de Boer
We provide a sound and relatively complete Hoare-like proof system for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-va…
Interacting via the Heap in the Presence of Recursion
Jurriaan Rot, Irina Măriuca Asăvoae, Frank de Boer +2
Almost all modern imperative programming languages include operations for dynamically manipulating the heap, for example by allocating and deallocating objects, and by updating ref…
Modular Verification of Recursive Programs
Krzysztof R. Apt, Frank S. de Boer, Ernst-Rüdiger Olderog
We argue that verification of recursive programs by means of the assertional method of C.A.R. Hoare can be conceptually simplified using a modular reasoning. In this approach some…
Proving correctness of Timed Concurrent Constraint Programs
F. S. de Boer, M. Gabbrielli, M. C. Meo
A temporal logic is presented for reasoning about the correctness of timed concurrent constraint programs. The logic is based on modalities which allow one to specify what a proces…