collaborators

1 paper

cs.LO2018

Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle

Bohua Zhan, Maximilian P. L. Haslbeck

We present a framework in Isabelle for verifying asymptotic time complexity of imperative programs. We build upon an extension of Imperative HOL and its separation logic to include…