Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Iptables_Semantics/   (Sammlung formaler Beweise Version 2026-5©)  Datei vom 31.4.2026 mit Größe 2 kB image not shown  

Quelle  ROOT

  Sprache: Text
 

chapter AFP

session Iptables_Semantics = Routing +
  options [timeout = 1200]
  sessions
    Native_Word
  directories
    "Common"
    "Semantics_Ternary"
    "Primitive_Matchers"
    "Simple_Firewall"
  theories [document = false]
    "Common/List_Misc"
    "Common/WordInterval_Lists"
  theories
    Semantics
    Example_Semantics
    Alternative_Semantics
    Semantics_Stateful
    Semantics_Goto
    Call_Return_Unfolding
    "Common/Negation_Type_DNF"
    "Semantics_Ternary/Semantics_Ternary"
    Matching_Embeddings
    Semantics_Embeddings
    Iptables_Semantics
    Semantics_Stateful
    "Semantics_Ternary/Optimizing"
    "Primitive_Matchers/No_Spoof"
    "Primitive_Matchers/Parser6"
    No_Spoof_Embeddings
    "Primitive_Matchers/Routing_IpAssmt"
    "Primitive_Matchers/Transform"
    "Primitive_Matchers/Primitive_Abstract"
    "Primitive_Matchers/Code_Interface"
    "Primitive_Matchers/Parser"
    "Simple_Firewall/SimpleFw_Compliance"
    Code_haskell
    Access_Matrix_Embeddings
    No_Spoof_Embeddings
    Documentation
  document_files
    "root.tex"
    "root.bib"

session Iptables_Semantics_Examples in "Examples" = Iptables_Semantics +
  options [timeout = 2400]
  directories
    "Parser_Test"
    "Fail"
    "Contrived"
    "Synology_Diskstation_DS414"
    "Ringofsaturn_com"
    "SQRL_Shorewall"
    "sns.ias.edu"
    "medium-sized-company"
  theories
    "Parser_Test/Parser_Test"
    "Parser_Test/Parser6_Test"
    "Small_Examples"
    "Fail/Ports_Fail"
    "Contrived/Contrived_Example"
    "Synology_Diskstation_DS414/Analyze_Synology_Diskstation"
    "Ringofsaturn_com/Analyze_Ringofsaturn_com"
    "SQRL_Shorewall/Analyze_SQRL_Shorewall"
    "SQRL_Shorewall/SQRL_2015_nospoof"
    "sns.ias.edu/SNS_IAS_Eduroam_Spoofing"
    "medium-sized-company/Analyze_medium_sized_company"
  document_files (in "../document")
    "root.tex"
    "root.bib"

session Iptables_Semantics_Examples_Big (slow very_slow) in "Examples_Big" = Iptables_Semantics_Examples +
  options [timeout = 60000]
  directories
    "../Examples/IPPartEval"
    "../Examples/TUM_Net_Firewall"
    "../Examples/containern"
    "../Examples/topoS_generated"
  theories
    "../Examples/topoS_generated/Analyze_topos_generated"
    "../Examples/IPPartEval/IP_Address_Space_Examples_All_Small"
    "../Examples/TUM_Net_Firewall/Analyze_TUM_Net_Firewall"
    "../Examples/containern/Analyze_Containern"
    "../Examples/TUM_Net_Firewall/TUM_Spoofing_new3"
    "../Examples/TUM_Net_Firewall/TUM_Simple_FW"
    "../Examples/IPPartEval/IP_Address_Space_Examples_All_Large"
  document_files (in "../document")
    "root.tex"
    "root.bib"

Messung V0.5 in Prozent
C=93 H=99 G=95

¤ Dauer der Verarbeitung: 0.9 Sekunden  (vorverarbeitet am  2026-06-10) ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.