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.Examples.Embedded
Strata.Examples.EmbeddedData
Strata.Languages.B3
Strata.Languages.GOTO
Strata.Pipeline.Diagnostic
Strata.Transform.CallElimCorrect
Strata.Transform.CoreSpecification
Strata.Transform.CoreTransformProps
Strata.Transform.DetToKleeneCorrect
Strata.Transform.FunctionInlining
Strata.Transform.FunctionInliningProps
Strata.Transform.LiftInternalFuncDecls
Strata.Transform.LiftInternalFuncDeclsCorrect
Strata.Transform.LoopInitHoist
Strata.Transform.LoopInitHoistCorrect
Strata.Transform.NondetElim
Strata.Transform.NondetElimCorrect
Strata.Transform.NondetElimProps
Strata.Transform.ProcBodyVerifyCorrect
Strata.Transform.StructuredToUnstructured
Strata.Transform.StructuredToUnstructuredCorrect
Strata.Transform.StructuredToUnstructuredPipeline
Strata.Transform.StructuredToUnstructuredPipelineCorrect
Strata.Util.NameProofs
Strata.Util.OrderedSetProps
Strata.Util.Random
Strata.Util.Sarif
StrataDDM.Integration.Lean
Strata.DL.Imperative.CFGSemantics
Strata.DL.Imperative.CFGSemanticsProps
Strata.DL.Lambda.DatatypeWF
Strata.DL.Lambda.LExprTProps
Strata.DL.Lambda.LExprTypeSpec
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.DatatypeTypeSpec
Strata.Languages.Core.EntryPoint
Strata.Languages.Core.FactoryWF
Strata.Languages.Core.ProcedureProps
Strata.Languages.Core.ProcedureTypeSpec
Strata.Languages.Core.ProgramTypeSpec
Strata.Languages.Core.ProgramWF
Strata.Languages.Core.SMTEncoderProps
Strata.Languages.Core.SarifOutput
Strata.Languages.Core.SeqModel
Strata.Languages.Core.StatementSemantics
Strata.Languages.Core.StatementWF
Strata.Languages.Core.VerifierProofs
Strata.Languages.Core.WFProps
Strata.Languages.Dyn.Dyn
Strata.Languages.Dyn.Verify
Strata.Languages.Laurel.FilterPrelude
Strata.Languages.Laurel.Grammar
Strata.Languages.Laurel.LaurelCompilationPipeline
Strata.Languages.Laurel.MonomorphizeCompositesProps
Strata.Languages.Laurel.ResolutionProps
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
Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslatorProps
Imported by