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

Citations by Year