Auditing User-Provided Axioms in Software Verification Conditions

Autor: Jackson, Paul, Schanda, Florian, Wallenburg, Angela

Publikováno v: Jackson, P, Schanda, F & Wallenburg, A 2013, Auditing User-Provided Axioms in Software Verification Conditions . in C Pecheur & M Dierkes (eds), Formal Methods for Industrial Critical Systems : 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013. Proceedings . vol. 8187, Lecture Notes in Computer Science, vol. 8187, Springer-Verlag GmbH, pp. 154-168 . https://doi.org/10.1007/978-3-642-41010-9_11

A common approach to formally checking assertions inserted into a program is to first generate verification conditions, logical sentences that, if then proven, ensure the assertions are correct. Sometimes users provide axioms that get incorporated in

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od______3094::4260ab4bca82acf8d989069d792e2334
https://hdl.handle.net/20.500.11820/dca91907-3600-4aa8-967c-c5f6e26b06cc

Class-local object invariants.

Autor: Leino, K. Rustan M., Wallenburg, Angela

Publikováno v: Proceedings of the 1st India Software Engineering Conference; 2/19/2008, p57-66, 10p

Proving by Induction.

Autor: Carbonell, Jaime G., Siekmann, Jörg, Beckert, Bernhard, Hähnle, Reiner, Schmitt, Peter H., Wallenburg, Angela

Publikováno v: Verification of Object-Oriented Software. The KeY Approach; 2006, p453-479, 27p