CIFASIS   20631
CENTRO INTERNACIONAL FRANCO ARGENTINO DE CIENCIAS DE LA INFORMACION Y DE SISTEMAS
Unidad Ejecutora - UE
artículos
Título:
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Autor/es:
DUMITRESCU, VICTOR; HRITCU, CATALIN; PIT-CLAUDEL, CLÉMENT; RASTOGI, ASEEM; AHMAN, DANEL; HAWBLITZEL, CHRIS; PARASKEVOPOULOU, ZOE; RAMANANANDRO, TAHINA; MARTÍNEZ, GUIDO; GIANNARAKIS, NICK; NARASIMHAMURTHY, MONAL; PROTZENKO, JONATHAN; SWAMY, NIKHIL
Revista:
LECTURE NOTES IN COMPUTER SCIENCE
Editorial:
Springer Verlag
Referencias:
Lugar: Praga; Año: 2019 vol. 1142 p. 30 - 59
ISSN:
0302-9743
Resumen:
We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of 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.