NREST: Nondeterministc RESult monad with Time

Abstract

This entry introduces NREST, a nondeterministc result monad with time, which was spun off a development of a framework for verifying functional correctness and worst-case complexity of algorithms refined down to LLVM, due to Haslbeck and Lammich.

License

BSD License

Topics

Computer science/Semantics and reasoning

Related publications

Haslbeck, M. P. L., & Lammich, P. (2022). For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM. ACM Transactions on Programming Languages and Systems, 44(3), 1–36. https://doi.org/10.1145/3486169
Haslbeck, M. P. L., & Lammich, P. (2021). For a Few Dollars More. Programming Languages and Systems, 292–319. https://doi.org/10.1007/978-3-030-72019-3_11

Session NREST

NREST_Auxiliaries
NREST
DataRefinement
RefineMonadicVCG
SepLogic_Misc
Refine_Foreach

Depends on

Automatic Data Refinement
Generating Cases from Labeled Subgoals
Refinement for Monadic Programs