Details

Autor(en) / Beteiligte

• Heisel, M.
• Reif, W.
• Stephan, W.

Titel

Tactical theorem proving in program verification

Ist Teil von

• 10th International Conference on Automated Deduction, 2005, p.117-131

Ort / Verlag

Berlin, Heidelberg: Springer Berlin Heidelberg

Erscheinungsjahr

2005

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• A "shell" for program verification and development is presented which is obtained by using a variant of Dynamic Logic in combination with tactical theorem proving. This shell (Karlsruhe Interactive Verifier) allows easy implementations of various strategies which are guaranteed to be correct with respect to the basic logic. It is shown how tactical theorem proving is adapted for the above purposes.