×

Fiat

swMATH ID: 21357
Software Authors: Delaware, B., Claudel, C.P., Gross, J., Chlipala, A.
Description: Fiat is a library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications. Programming by Fiat starts with a high-level description of a program, which can be written using libraries of specification languages for describing common programming tasks like querying a relational database. These specifications are then iteratively refined into efficient implementations via automated tactics. Each derivation in Fiat produces a formal proof trail certifying that the synthesized program meets the original specification. Code synthesized by Fiat can be extracted to an equivalent OCaml program that can be compiled and run as normal.
Homepage: http://plv.csail.mit.edu/fiat/
Dependencies: Coq
Related Software: Coq; Isabelle/HOL; CakeML; Isabelle; CertiCoq; OCaml; Autoref; Gabow SCC; CAVA LTL Modelchecker; Archive Formal Proofs; Dijkstra Shortest Path; CeTA; HOL; PVS; Why3; Coq/SSReflect; Theorema; Mathematica; seL4; Toolchain
Cited in: 16 Documents

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Fiat: deductive synthesis of abstract data types in a proof assistant. Zbl 1346.68175
Delaware, Benjamin; Pit-Claudel, Clément; Gross, Jason; Chlipala, Adam
2015
all top 5

Cited by 32 Authors

3 Lochbihler, Andreas
2 Chlipala, Adam J.
2 Dagand, Pierre-Evariste
2 Delaware, Benjamin
2 Drămnesc, Isabela
2 Gross, Jason
2 Jebelean, Tudor
2 Kumar, Ramana
2 Lammich, Peter
2 Myreen, Magnus O.
2 Pit-Claudel, Clément
2 Stratulat, Sorin
1 Bengtson, Jesper
1 Benzaken, Véronique
1 Blot, Arthur
1 Contejean, Evelyne
1 Costea, Andreea
1 Darais, David
1 Guéneau, Armaël
1 Lawall, Julia L.
1 Malecha, Gregory
1 Mullen, Eric
1 Norrish, Michael
1 Polikarpova, Nadia
1 Schneider, Joshua P.
1 Sergey, Ilya
1 Tabareau, Nicolas
1 Tanter, Éric
1 Tatlock, Zachary
1 VanHorn, David A.
1 Wang, Peng
1 Zhu, Amy

Cited in 3 Serials

2 Journal of Automated Reasoning
2 Journal of Functional Programming
1 Journal of Symbolic Computation

Cited in 2 Fields

16 Computer science (68-XX)
1 Order, lattices, ordered algebraic structures (06-XX)

Citations by Year