Documentation
Strata
Search
return to top
source
Imports
Init
StrataDDM
Strata.MetaVerifier
Strata.SimpleAPI
StrataDDM.Ion
Strata.Backends.CBMC
Strata.Cli.Framework
Strata.Cli.VerifyOptions
Strata.DL.Imperative
Strata.DL.Lambda
Strata.DL.SMT
Strata.Languages.B3
Strata.Pipeline.Diagnostic
Strata.Transform.CallElimCorrect
Strata.Transform.CoreSpecification
Strata.Transform.DetToKleeneCorrect
Strata.Transform.ProcBodyVerifyCorrect
Strata.Transform.StructuredToUnstructured
Strata.Util.NameProofs
Strata.Util.Random
Strata.Util.Sarif
StrataDDM.Integration.Lean
Strata.DL.Imperative.CFGSemantics
Strata.DL.Imperative.CFGToCProverGOTO
Strata.DL.Imperative.ToCProverGOTO
Strata.DL.Lambda.LExprTypeSpec
Strata.DL.Lambda.MetaData
Strata.DL.Lambda.Reflect
Strata.DL.Lambda.Semantics
Strata.DL.Lambda.TypeFactoryWF
Strata.DL.SMT.Denote
Strata.DL.SMT.FactoryCorrect
Strata.DL.SMT.Translate
Strata.DL.Util.HList
Strata.Languages.C_Simp.C_Simp
Strata.Languages.C_Simp.Verify
Strata.Languages.Core.EntryPoint
Strata.Languages.Core.FactoryWF
Strata.Languages.Core.ProgramWF
Strata.Languages.Core.SarifOutput
Strata.Languages.Core.SeqModel
Strata.Languages.Core.StatementSemantics
Strata.Languages.Core.StatementWF
Strata.Languages.Core.VerifierProofs
Strata.Languages.Dyn.Dyn
Strata.Languages.Dyn.Verify
Strata.Languages.Laurel.FilterPrelude
Strata.Languages.Laurel.Grammar
Strata.Languages.Laurel.LaurelCompilationPipeline
Strata.DL.Lambda.Denote.Assumptions
Strata.DL.Lambda.Denote.CallOfLFuncDenote
Strata.DL.Lambda.Denote.LExprDenote
Strata.DL.Lambda.Denote.LExprDenoteConstrs
Strata.DL.Lambda.Denote.LExprDenoteEq
Strata.DL.Lambda.Denote.LExprDenoteProps
Strata.DL.Lambda.Denote.LExprDenoteSubst
Strata.DL.Lambda.Denote.LExprDenoteTySubst
Strata.DL.Lambda.Denote.LExprSemanticsConsistent
Strata.Languages.Dyn.DDMTransform.Parse
Strata.Languages.Dyn.DDMTransform.Translate
Imported by