Verifying asymptotic time complexity of imperative programs in Isabelle

DOI10.1007/978-3-319-94205-6_35OpenAlexW2964083189MaRDI QIDQ1799114

Bohua Zhan, Maximilian P. L. Haslbeck

Publication date: 18 October 2018

Full work available at URL: https://arxiv.org/abs/1802.01336

zbMATH Keywords

separation logicprogram verificationIsabelletime complexity analysis

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Denotational semantics as a foundation for cost recurrence extraction for functional languages ⋮ Unnamed Item ⋮ For a few dollars more. Verified fine-grained algorithm analysis down to LLVM

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• AUTO2
• TiML
• Separation Logic
• Berlekamp Zassenhaus
• Landau Symbols
• Median-of-Medians
• Auto2_Imperative_HOL

This page was built for publication: Verifying asymptotic time complexity of imperative programs in Isabelle