Documentation
Strata
Search
return to top
source
Imports
Init
StrataDDM
Strata.MetaVerifier
Strata.SimpleAPI
StrataDDM.Ion
Strata.Backends.CBMC
Strata.Cli.CoreCommands
Strata.Cli.DialectCommands
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.Cortex
Strata.Languages.GOTO
Strata.Pipeline.Diagnostic
Strata.Pipeline.FactSet
Strata.Pipeline.FactSetProps
Strata.Pipeline.PhaseContract
Strata.Pipeline.PhaseContractProps
Strata.Transform.CallElimCorrect
Strata.Transform.CoreSpecHoareConnection
Strata.Transform.CoreSpecification
Strata.Transform.CoreSpecificationProps
Strata.Transform.CoreTransformProps
Strata.Transform.DeadDefElimCoreCorrect
Strata.Transform.DetToKleeneCorrect
Strata.Transform.EqualitySimplificationCorrect
Strata.Transform.FoldAxiomsEntry
Strata.Transform.FunctionInlining
Strata.Transform.FunctionInliningProps
Strata.Transform.InsertLoopInvariantAssertsCoreCorrect
Strata.Transform.LoopElimCoreCorrect
Strata.Transform.LoopInitHoist
Strata.Transform.LoopInitHoistCoreCorrect
Strata.Transform.LoopInitHoistCorrect
Strata.Transform.LoopInitHoistProps
Strata.Transform.MonomorphizeBasics
Strata.Transform.MonomorphizeFunctionsCorrect
Strata.Transform.MonomorphizeInstances
Strata.Transform.MonomorphizeWorklist
Strata.Transform.NondetElim
Strata.Transform.NondetElimCoreCorrect
Strata.Transform.NondetElimCorrect
Strata.Transform.NondetElimProps
Strata.Transform.ProcBodyVerifyCorrect
Strata.Transform.RecursiveFunctionAxioms
Strata.Transform.Simplify
Strata.Transform.SpecHoareConnection
Strata.Transform.StructuredToUnstructured
Strata.Transform.StructuredToUnstructuredCoreCorrect
Strata.Transform.StructuredToUnstructuredCorrect
Strata.Transform.StructuredToUnstructuredPipeline
Strata.Transform.StructuredToUnstructuredPipelineCoreCorrect
Strata.Transform.StructuredToUnstructuredPipelineCorrect
Strata.Transform.StructuredToUnstructuredPipelineProps
Strata.Transform.StructuredToUnstructuredProps
Strata.Transform.UnrollBoundedQuantifiersProps
Strata.Util.HListProps
Strata.Util.HMapsProps
Strata.Util.IonDeserializer
Strata.Util.LeftistHeapProps
Strata.Util.NameProofs
Strata.Util.OrderedSetProps
Strata.Util.Random
Strata.Util.RealProps
Strata.Util.RopeProps
Strata.Util.Sarif
Strata.Util.Worklist
StrataDDM.Integration.Lean
Strata.DL.Imperative.InterpreterFuelMono
Strata.DL.Imperative.InterpreterTowerProps
Strata.DL.Imperative.StmtExtendCallBridge
Strata.DL.Lambda.DatatypeFactoryWFProps
Strata.DL.Lambda.DatatypeWF
Strata.DL.Lambda.KnownTypesProps
Strata.DL.Lambda.LExprDenoteEval
Strata.DL.Lambda.LExprDenoteEvalProps
Strata.DL.Lambda.LExprEvalAnnotateProps
Strata.DL.Lambda.LExprEvalFuelProps
Strata.DL.Lambda.LExprEvalFully
Strata.DL.Lambda.LExprEvalSound
Strata.DL.Lambda.LExprRenameOps
Strata.DL.Lambda.LExprTProps
Strata.DL.Lambda.LExprTraversal
Strata.DL.Lambda.LExprTraversalProps
Strata.DL.Lambda.LExprTypeEnvProps
Strata.DL.Lambda.LExprTypeSpec
Strata.DL.Lambda.LFuncEvalSound
Strata.DL.Lambda.NamePrefixesProps
Strata.DL.Lambda.OperationalSemantics
Strata.DL.Lambda.OperationalSemanticsProps
Strata.DL.Lambda.Reflect
Strata.DL.Lambda.TypeFactoryWF
Strata.DL.SMT.Denote
Strata.DL.SMT.DenoteProps
Strata.DL.SMT.DenoteSemanticsEquiv
Strata.DL.SMT.DenoteTyped
Strata.DL.SMT.DenoteTypedProps
Strata.DL.SMT.DenoteTypedSMTQuery
Strata.DL.SMT.FactoryCorrect
Strata.DL.SMT.RegexMatchProps
Strata.DL.SMT.SymbolProps
Strata.DL.SMT.Translate
Strata.Languages.Core.BitVecEvalProps
Strata.Languages.Core.ConfigWF
Strata.Languages.Core.DatatypeTypeSpec
Strata.Languages.Core.DatatypeTypeSpecProps
Strata.Languages.Core.DeclFormulas
Strata.Languages.Core.EntryPoint
Strata.Languages.Core.EnvProps
Strata.Languages.Core.FactoryEvalSoundWF
Strata.Languages.Core.FactoryProps
Strata.Languages.Core.FactoryWF
Strata.Languages.Core.IncrementalSolve
Strata.Languages.Core.IncrementalSolveCorrect
Strata.Languages.Core.InstExprTyping
Strata.Languages.Core.InstWellFormedSemanticsEval
Strata.Languages.Core.IntEvalProps
Strata.Languages.Core.Interpreter
Strata.Languages.Core.InterpreterBridgeStatements
Strata.Languages.Core.InterpreterCFG
Strata.Languages.Core.InterpreterCFGProps
Strata.Languages.Core.InterpreterCallComplete
Strata.Languages.Core.InterpreterCallSound
Strata.Languages.Core.InterpreterComplete
Strata.Languages.Core.InterpreterDomainProps
Strata.Languages.Core.InterpreterEval
Strata.Languages.Core.InterpreterEvalProps
Strata.Languages.Core.InterpreterEvalSound
Strata.Languages.Core.InterpreterKleene
Strata.Languages.Core.InterpreterKleeneProps
Strata.Languages.Core.InterpreterObs
Strata.Languages.Core.InterpreterObsProps
Strata.Languages.Core.InterpreterReach
Strata.Languages.Core.InterpreterReachBridge
Strata.Languages.Core.InterpreterReachBuiltins
Strata.Languages.Core.InterpreterReachCheck
Strata.Languages.Core.InterpreterReplayTactics
Strata.Languages.Core.InterpreterSound
Strata.Languages.Core.PipelinePhaseProps
Strata.Languages.Core.ProcedureProps
Strata.Languages.Core.ProcedureTypeProps
Strata.Languages.Core.ProcedureTypeSpec
Strata.Languages.Core.ProgramFact
Strata.Languages.Core.ProgramFactProps
Strata.Languages.Core.ProgramFactSet
Strata.Languages.Core.ProgramFactSetProps
Strata.Languages.Core.ProgramProps
Strata.Languages.Core.ProgramTypeSpec
Strata.Languages.Core.ProgramWF
Strata.Languages.Core.ReplayWF
Strata.Languages.Core.SMTEmitter
Strata.Languages.Core.SMTEncoderProps
Strata.Languages.Core.SarifOutput
Strata.Languages.Core.SeqModel
Strata.Languages.Core.StatementProps
Strata.Languages.Core.StatementSemantics
Strata.Languages.Core.StatementWF
Strata.Languages.Core.StmtCallFree
Strata.Languages.Core.StmtExtendCallBridgeProps
Strata.Languages.Core.VerifierProofs
Strata.Languages.Core.WFProps
Strata.Transform.Passive.CoreProgram
Strata.Transform.Passive.CoreProgramProps
Strata.Transform.Passive.CoreTyped
Strata.Transform.Passive.CoreWPSSA
Strata.Transform.Passive.CoreWPSSAProps
Strata.Transform.Passive.DeclObligationsCoreCorrect
Strata.Transform.Passive.Over
Strata.Transform.SSA.SSACoreCorrect
Strata.Transform.SSA.SSACoreProgram
Strata.Transform.SSA.SSACoreProgramProps
Strata.Transform.SSA.SSAEval
Strata.Transform.SSA.SSAOver
Strata.Transform.Simplify.DeadDefsShape
Strata.Transform.Simplify.Expr
Strata.Transform.Simplify.LiveSweep
Strata.Transform.Simplify.StmtShape
Strata.Transform.WP.WPCoreCorrect
Strata.Transform.WP.WPCoreDefs
Strata.Transform.WP.WPCoreGate
Strata.Transform.WP.WPCoreOps
Strata.Transform.WP.WPCorePrefix
Strata.Transform.WP.WPCoreProgram
Strata.Transform.WP.WPCoreProgramProps
Strata.Transform.WP.WPCoreTyping
Strata.Transform.WP.WPEvalIface
Strata.Transform.WP.WPOutDecls
Strata.Transform.WP.WPOutOps
Strata.Transform.WP.WPOutSyntax
Strata.Transform.WP.WPOutTypes
Strata.Transform.WP.WPOutTyping
Strata.Transform.WP.WPOutTypingWalk
Strata.Transform.WP.WPProps
Strata.Transform.WP.WPReplay
Strata.Transform.WP.WPRestrict
Strata.DL.Imperative.Logic.HoareTemplate
Strata.DL.Lambda.Denote.Assumptions
Strata.DL.Lambda.Denote.CallOfLFuncDenote
Strata.DL.Lambda.Denote.LExprDenote
Strata.DL.Lambda.Denote.LExprDenoteCompute
Strata.DL.Lambda.Denote.LExprDenoteConstrs
Strata.DL.Lambda.Denote.LExprDenoteConsts
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.Analysis.DeductiveVerification
Strata.Languages.Core.Analysis.DeductiveVerificationProps
Strata.Languages.Core.Analysis.FragmentFactory
Strata.Languages.Core.Analysis.ProcedureCorrectness
Strata.Languages.Core.Analysis.ProcedureCorrectnessProps
Strata.Languages.Core.Logic.ContractToHoareTriple
Strata.Languages.Core.Logic.ContractToHoareTripleProps
Strata.Languages.Core.Logic.FactoryInterp
Strata.Languages.Core.Logic.Hoare
Strata.Languages.Core.Logic.HoareCall
Strata.Languages.Core.Logic.LangDefProps
Strata.Languages.Core.Logic.TraceInterpUsingDenote
Strata.Languages.Core.Logic.TraceInterpUsingDenoteProps
Strata.Languages.Core.Typing.Props.FactoryRegistrationProps
Strata.Languages.Core.Typing.Props.ProcSigAgreementProps
Strata.Languages.Core.Typing.Props.TypingSpecProps
Strata.Languages.Core.Typing.Spec.TypeSpecShared
Strata.Languages.Core.Typing.Spec.TypingSpec
Imported by