Session Formal_SSA

Theories

• HOL-Library.Sublist
• FormalSSA_Misc
• Serial_Rel
• HOL-Library.Mapping
• Mapping_Exts
• HOL-Library.RBT_Mapping
• HOL-Library.RBT_Set
• RBT_Mapping_Exts
• Dijkstra_Shortest_Path.Graph
• Dijkstra_Shortest_Path.GraphSpec
• HOL-Library.Omega_Words_Fun
• CAVA_Automata.Digraph_Basic
• Graph_path
• SSA_CFG
• Minimality
• Construct_SSA
• Construct_SSA_notriv
• SSA_Semantics
• While_Combinator_Exts
• SSA_CFG_code
• Construct_SSA_code
• SSA_Transfer_Rules
• Construct_SSA_notriv_code
• Generic_Interpretation
• Generic_Extract
• Slicing.Com
• Slicing.AuxLemmas
• Slicing.BasicDefs
• Slicing.WCFG
• Slicing.CFG
• Slicing.CFGExit
• Slicing.Interpretation
• Slicing.Labels
• Slicing.CFG_wf
• Slicing.CFGExit_wf
• Slicing.Observable
• Slicing.Distance
• Slicing.DynDataDependence
• Slicing.DataDependence
• Slicing.SemanticsCFG
• Slicing.Slice
• Slicing.Postdomination
• Slicing.DynStandardControlDependence
• Slicing.StandardControlDependence
• Slicing.DynWeakControlDependence
• Slicing.WeakControlDependence
• Slicing.PDG
• Slicing.WeakOrderDependence
• Slicing.CDepInstantiations
• Slicing.WellFormed
• Slicing.AdditionalLemmas
• Disjoin_Transform
• HOL-Library.List_Lexorder
• HOL-Library.Char_ord
• WhileGraphSSA