Using a program verification calculus for constructing specifications from implementations

In this thesis we examine the possibility of
automatically constructing the program specification
from an implementation, both from a theoretical
perspective and as a practical approach with a sequent
calculus. As a setting for program specifications we
choose dynamic logic for the Java programming language.
We show that—despite the undecidable nature of
program analysis—the strongest specification of any
program can always be constructed algorithmically.
Further we outline a practical approach embedded into a
sequent calculus for dynamic logic and with a higher
focus on readability. Therefor, the central aspect of
describing unbounded state changes incorporates the
concept of modifies lists for expressing the modifiable
portion of the state space. The underlying deductions
are carried out by the theorem prover of the KeY
System.

@misc{Platzer_2004,
	author = {['André Platzer']},
	title = {Using a Program Verification Calculus for
               Constructing Specifications from
               Implementations},
	howpublished = {Minor thesis,
        University of Karlsruhe, Department of Computer
        Science. Institute for Logic, Complexity and
        Deduction Systems},
	month = {February},
	year = {2004},
	school = {University of Karlsruhe, Department of
               Computer Science. Institute for Logic,
               Complexity and Deduction Systems},
	pages = {83},
	abstract = {
    In this thesis we examine the possibility of
    automatically constructing the program specification
    from an implementation, both from a theoretical
    perspective and as a practical approach with a sequent
    calculus. As a setting for program specifications we
    choose dynamic logic for the Java programming language.
    We show that—despite the undecidable nature of
    program analysis—the strongest specification of any
    program can always be constructed algorithmically.
    Further we outline a practical approach embedded into a
    sequent calculus for dynamic logic and with a higher
    focus on readability. Therefor, the central aspect of
    describing unbounded state changes incorporates the
    concept of modifies lists for expressing the modifiable
    portion of the state space. The underlying deductions
    are carried out by the theorem prover of the KeY
    System.
    },
	pdf = {https://lfcps.org/logic/Minoranthe.pdf},
	slides = {https://lfcps.org/logic/Minoranslides.pdf}
}