@inproceedings{martnez2019meta-f,
author = {Martínez, Guido and Ahman, Danel and Dumitrescu, Victor and Giannarakis, Nick and Hawblitzel, Chris and Hritcu, Catalin and Narasimhamurthy, Monal and Paraskevopoulou, Zoe and Pit-Claudel, Clément and Protzenko, Jonathan and Ramananandro, Tahina and Rastogi, Aseem and Swamy, Nikhil},
title = {Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms},
booktitle = {ESOP 2019},
year = {2019},
month = {April},
abstract = {We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing to use tactics and metaprogramming to discharge assertions not solvable by SMT, or to just simplify them into well-behaved SMT fragments. Plus, Meta-F* can be used to generate verified code automatically.

Meta-F* is implemented as an F* effect, which, given the powerful effect system of F*, heavily increases code reuse and even enables the lightweight verification of metaprograms. Metaprograms can be either interpreted, or compiled to efficient native code that can be dynamically loaded into the F* type-checker and can interoperate with interpreted code. Evaluation on realistic case studies shows that Meta-F* provides substantial gains in proof development, efficiency, and robustness.},
url = {http://approjects.co.za/?big=en-us/research/publication/meta-f-proof-automation-with-smt-tactics-and-metaprograms-2/},
}