A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification

Abstract : We present a framework for simultaneously verifying the functional correctness and the worst-case asymptotic time complexity of higher-order imperative programs. We build on top of Separation Logic with Time Credits, embedded in an interactive proof assistant. We formalize the O notation, which is key to enabling modular specifications and proofs. We cover the subtleties of the multivariate case, where the complexity of a program fragment depends on multiple parameters. We propose a way of integrating complexity bounds into specifications, present lemmas and tactics that support a natural reasoning style, and illustrate their use with a collection of examples.
Type de document :
Communication dans un congrès
Amal Ahmed. ESOP 2018 - 27th European Symposium on Programming, Apr 2018, Thessaloniki, Greece. Springer, 10801, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-319-89884-1_19〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01926485
Contributeur : François Pottier <>
Soumis le : lundi 19 novembre 2018 - 11:45:45
Dernière modification le : lundi 26 novembre 2018 - 13:28:01

Fichier

gueneau-chargeraud-pottier-eso...
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Armaël Guéneau, Arthur Charguéraud, François Pottier. A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. Amal Ahmed. ESOP 2018 - 27th European Symposium on Programming, Apr 2018, Thessaloniki, Greece. Springer, 10801, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-319-89884-1_19〉. 〈hal-01926485〉

Partager

Métriques

Consultations de la notice

45

Téléchargements de fichiers

32