2015/01/18 by Maria Pelevina, Pelevina, Maria
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Software Engineering (cs.SE) #cs.SE
paper · pdf · doi:10.48550/arxiv.1501.04359
arxiv created 2015/01/18 · openalex publication_date 2015/01/18 · arxiv updated 2015/01/20 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/28
For engineering software with formal correctness proofs it is crucial that proofs can be efficiently reused in case the software or its specification is changed. Unfortunately, in reality even slight changes in the code or its specification often result in disproportionate waste of verification effort: For instance, whenever a method's specification is modified and as a consequence the proof of its correctness breaks, all other proofs based on this specification break too. Abstract method calls is a recently proposed verification rule for method calls that allows for efficient systematic reuse of proofs. In this thesis, we implement, extend and evaluate this approach within the KeY verification system.