Understanding parameters of deductive verification: an empirical investigation of KeY

DOI10.1007/978-3-319-94821-8_20MaRDI QIDQ1791175

Ina Schaefer, Thomas Thüm, Alexander Knüppel, Carsten Immanuel Pardylla

Publication date: 4 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94821-8_20

zbMATH Keywords

theorem proving; automated reasoning; formal methods; control parameters; deductive verification; design by contract; KeY

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Uses Software

• KRAKATOA
• Why3
• JML
• Spec#
• Caduceus
• Frama-C
• z3
• VCC
• Java PathFinder
• KeY
• SPL Conqueror