CFML

MaRDI QIDQ25202swMATHFDO

Official website http://dl.acm.org/citation.cfm?doid=1863543.1863590

Described by source

• Program verification through characteristic formulae

Cited in

(45)

• Netsoft
• Crowfoot
• IsaFoR
• Ynot
• RGITL
• GNATprove
• MLton
• Symbolic execution proofs for higher order store programs
• Proof-producing translation of higher-order logic into pure and stateful ML
• AUTO2
• Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
• Cogent
• Fiat
• Ssreflect.fintype
• MathComp.tuple
• VACID-0
• CAMPY
• ACE
• CSimpl
• Grail
• An observationally complete program logic for imperative higher-order functions
• TiML
• VST-Floyd
• Camelot
• Edmonds-Karp
• Separation Logic
• Dijkstra Shortest Path
• Refinement Monadic
• Flow Networks
• Graph Theory
• Amortized Complexity
• Collections
• Equations
• CAVA LTL Modelchecker
• Gabow SCC
• Imperative Refinement
• Maximum Cardinality Matching
• ShortestPath
• Auto2_Imperative_HOL
• Dune
• Proof-producing synthesis of ML from higher-order logic
• Characteristic formulae for the verification of imperative programs
• FreeSpec
• Prpu_Maxflow
• HolBA

This page was built for software: CFML