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.Pipeline.FactSet
Strata.Pipeline.FactSetProps
Strata.Pipeline.PhaseContract
Strata.Pipeline.PhaseContractProps
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.SpecHoareConnection
Strata.Transform.StructuredToUnstructured
Strata.Transform.StructuredToUnstructuredCorrect
Strata.Transform.StructuredToUnstructuredPipeline
Strata.Transform.StructuredToUnstructuredPipelineCorrect
Strata.Transform.UnrollBoundedQuantifiersProps
Strata.Util.HListProps
Strata.Util.IonDeserializer
Strata.Util.NameProofs
Strata.Util.OrderedSetProps
Strata.Util.Random
Strata.Util.Sarif
Strata.Util.Worklist
StrataDDM.Integration.Lean
Strata.DL.Imperative.CFGSemantics
Strata.DL.Imperative.CFGSemanticsProps
Strata.DL.Lambda.DatatypeWF
Strata.DL.Lambda.LExprTProps
Strata.DL.Lambda.LExprTraversal
Strata.DL.Lambda.LExprTraversalProps
Strata.DL.Lambda.LExprTypeSpec
Strata.DL.Lambda.Reflect
Strata.DL.Lambda.Semantics
Strata.DL.Lambda.TypeFactoryWF
Strata.DL.SMT.Denote
Strata.DL.SMT.DenoteSemanticsEquiv
Strata.DL.SMT.DenoteTyped
Strata.DL.SMT.DenoteTypedProps
Strata.DL.SMT.DenoteTypedSMTQuery
Strata.DL.SMT.FactoryCorrect
Strata.DL.SMT.SymbolProps
Strata.DL.SMT.Translate
Strata.Languages.C_Simp.C_Simp
Strata.Languages.C_Simp.Verify
Strata.Languages.Core.BitVecEvalProps
Strata.Languages.Core.DatatypeTypeSpec
Strata.Languages.Core.EntryPoint
Strata.Languages.Core.ExpressionsProps
Strata.Languages.Core.FactoryWF
Strata.Languages.Core.PipelinePhaseProps
Strata.Languages.Core.ProcedureProps
Strata.Languages.Core.ProcedureTypeSpec
Strata.Languages.Core.ProgramFact
Strata.Languages.Core.ProgramFactProps
Strata.Languages.Core.ProgramFactSet
Strata.Languages.Core.ProgramFactSetProps
Strata.Languages.Core.ProgramTypeSpec
Strata.Languages.Core.ProgramWF
Strata.Languages.Core.SMTEmitter
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.DL.Imperative.Logic.HoareTemplate
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.Core.Logic.ContractToHoareTriple
Strata.Languages.Core.Logic.ContractToHoareTripleProps
Strata.Languages.Core.Logic.Hoare
Strata.Languages.Core.Logic.HoareCall
Strata.Languages.Core.Logic.LangDefProps
Strata.Languages.Core.Logic.TraceInterpUsingDenote
Strata.Languages.Dyn.DDMTransform.Parse
Strata.Languages.Dyn.DDMTransform.Translate
Imported by