Archive of Formal Proofs

 

Test status of entries in the AFP development version

Isabelle revision: a77d54ef718b
AFP revision: ff2ae1f38b5e
Build time:Mon, 11 Dec 2017 19:44:58 GMT
Build URL:Jenkins
Job name:isabelle-repo-afp

 

[skipped] AODV
[ok] AVL-Trees
[ok] AWN
[ok] Abortable_Linearizable_Modules
[ok] Abs_Int_ITP2012
[ok] Abstract-Hoare-Logics
[ok] Abstract-Rewriting
[ok] Abstract_Completeness
[ok] Abstract_Soundness
[ok] Affine_Arithmetic
[ok] Akra_Bazzi
[ok] Algebraic_Numbers
[ok] Algebraic_VCs
[ok] Allen_Calculus
[ok] Amortized_Complexity
[ok] AnselmGod
[ok] Applicative_Lifting
[ok] ArrowImpossibilityGS
[ok] AutoFocus-Stream
[ok] Automatic_Refinement
[ok] BDD
[ok] Bell_Numbers_Spivey
[ok] Berlekamp_Zassenhaus
[ok] Bernoulli
[ok] Bertrands_Postulate
[ok] BinarySearchTree
[ok] Binomial-Heaps
[ok] Binomial-Queues
[ok] Bondy
[ok] Boolean_Expression_Checkers
[ok] Bounded_Deducibility_Security
[ok] Buchi_Complementation
[ok] Buffons_Needle
[ok] Buildings
[ok] BytecodeLogicJmlTypes
[ok] CAVA_Automata
[ok] CAVA_LTL_Modelchecker
[ok] CCS
[ok] CISC-Kernel
[ok] CRDT
[ok] CYK
[ok] Call_Arity
[ok] Card_Equiv_Relations
[ok] Card_Multisets
[ok] Card_Number_Partitions
[ok] Card_Partitions
[ok] Cartan_FP
[ok] Case_Labeling
[ok] Catalan_Numbers
[ok] Category
[ok] Category2
[ok] Category3
[ok] Cauchy
[ok] Cayley_Hamilton
[ok] Certification_Monads
[ok] Chord_Segments
[ok] Circus
[ok] ClockSynchInst
[ok] CofGroups
[ok] Coinductive
[ok] Coinductive_Languages
[ok] Collections
[ok] Comparison_Sort_Lower_Bound
[ok] Compiling-Exceptions-Correctly
[ok] Completeness
[ok] Complx
[ok] ComponentDependencies
[skipped] ConcurrentGC
[ok] ConcurrentIMP
[ok] Concurrent_Ref_Alg
[ok] Consensus_Refined
[ok] Constructor_Funs
[ok] Containers
[ok] CoreC++
[ok] Count_Complex_Roots
[ok] CryptHOL
[ok] CryptoBasedCompositionalProperties
[ok] DFS_Framework
[ok] DPT-SAT-Solver
[ok] DataRefinementIBP
[ok] Datatype_Order_Generator
[ok] Decl_Sem_Fun_PL
[ok] Decreasing-Diagrams
[ok] Decreasing-Diagrams-II
[ok] Deep_Learning
[ok] Density_Compiler
[ok] Dependent_SIFUM_Refinement
[ok] Dependent_SIFUM_Type_Systems
[ok] Depth-First-Search
[ok] Derangements
[ok] Deriving
[ok] Descartes_Sign_Rule
[ok] Dict_Construction
[ok] Differential_Dynamic_Logic
[ok] Dijkstra_Shortest_Path
[ok] Diophantine_Eqns_Lin_Hom
[ok] Dirichlet_Series
[ok] Discrete_Summation
[ok] DiskPaxos
[ok] DynamicArchitectures
[ok] Dynamic_Tables
[ok] E_Transcendental
[ok] Echelon_Form
[ok] EdmondsKarp_Maxflow
[ok] Efficient-Mergesort
[ok] Elliptic_Curves_Group_Law
[ok] Encodability_Process_Calculi
[ok] Ergodic_Theory
[ok] Euler_MacLaurin
[ok] Euler_Partition
[ok] FFT
[ok] FLP
[ok] FOL-Fitting
[ok] FOL_Harrison
[ok] FeatherweightJava
[ok] Featherweight_OCL
[ok] Fermat3_4
[ok] FileRefinement
[ok] FinFun
[ok] Finger-Trees
[ok] Finite_Automata_HF
[ok] First_Welfare_Theorem
[ok] Fisher_Yates
[ok] Flow_Networks
[ok] Floyd_Warshall
[skipped] Flyspeck-Tame
[ok] FocusStreamsCaseStudies
[ok] Formal_SSA
[ok] Formula_Derivatives
[ok] Free-Boolean-Algebra
[ok] Free-Groups
[ok] FunWithFunctions
[ok] FunWithTilings
[ok] Functional-Automata
[ok] GPU_Kernel_PL
[ok] Gabow_SCC
[ok] Game_Based_Crypto
[ok] Gauss-Jordan-Elim-Fun
[ok] Gauss_Jordan
[ok] GenClock
[ok] General-Triangle
[ok] Girth_Chromatic
[ok] GoedelGod
[ok] GraphMarkingIBP
[ok] Graph_Theory
[ok] Groebner_Bases
[ok] Group-Ring-Module
[ok] HOLCF-Prelude
[ok] HRB-Slicing
[ok] Heard_Of
[ok] HereditarilyFinite
[ok] Hermite
[ok] HotelKeyCards
[ok] Huffman
[ok] Hybrid_Multi_Lane_Spatial_Logic
[ok] HyperCTL
[ok] IEEE_Floating_Point
[ok] IMAP-CRDT
[ok] IP_Addresses
[ok] Imperative_Insertion_Sort
[ok] Impossible_Geometry
[ok] Incompleteness
[ok] Incredible_Proof_Machine
[ok] Inductive_Confidentiality
[ok] InfPathElimination
[ok] InformationFlowSlicing
[ok] InformationFlowSlicing_Inter
[ok] Integration
[ok] Iptables_Semantics
[ok] Isabelle_Meta_Model
[ok] Jinja
[skipped] JinjaThreads
[ok] JiveDataStoreModel
[ok] Jordan_Hoelder
[ok] Jordan_Normal_Form
[ok] KAD
[ok] KAT_and_DRA
[ok] KBPs
[ok] Key_Agreement_Strong_Adversaries
[ok] Kleene_Algebra
[ok] Knot_Theory
[ok] Koenigsberg_Friendship
[ok] Kuratowski_Closure_Complement
[ok] LOFT
[ok] LTL
[ok] LTL_to_DRA
[ok] LTL_to_GBA
[ok] Lam-ml-Normalization
[ok] LambdaMu
[ok] Lambda_Free_KBOs
[ok] Lambda_Free_RPOs
[ok] Landau_Symbols
[ok] Latin_Square
[ok] LatticeProperties
[ok] Launchbury
[ok] Lazy-Lists-II
[ok] Lazy_Case
[ok] Lehmer
[ok] Lifting_Definition_Option
[ok] LightweightJava
[ok] LinearQuantifierElim
[ok] Linear_Recurrences
[ok] Liouville_Numbers
[ok] List-Index
[ok] List-Infinite
[ok] List_Interleaving
[ok] List_Update
[ok] LocalLexing
[ok] Locally-Nameless-Sigma
[ok] Lowe_Ontological_Argument
[ok] Lower_Semicontinuous
[ok] Lp
[ok] MFMC_Countable
[ok] MSO_Regex_Equivalence
[ok] Markov_Models
[ok] Marriage
[ok] Matrix
[ok] Matrix_Tensor
[ok] Max-Card-Matching
[ok] Menger
[ok] MiniML
[ok] Minimal_SSA
[ok] Minkowskis_Theorem
[ok] Modal_Logics_for_NTS
[ok] Monad_Normalisation
[ok] MonoBoolTranAlgebra
[ok] MonoidalCategory
[ok] Monomorphic_Monad
[ok] MuchAdoAboutTwo
[ok] Multirelations
[ok] Myhill-Nerode
[ok] Name_Carrying_Type_Inference
[ok] Nat-Interval-Logic
[ok] Native_Word
[ok] Nested_Multisets_Ordinals
[ok] Network_Security_Policy_Verification
[ok] No_FTL_observers
[ok] Nominal2
[ok] Noninterference_CSP
[ok] Noninterference_Concurrent_Composition
[ok] Noninterference_Generic_Unwinding
[ok] Noninterference_Inductive_Unwinding
[ok] Noninterference_Ipurge_Unwinding
[ok] Noninterference_Sequential_Composition
[ok] NormByEval
[ok] Open_Induction
[ok] Optics
[ok] Orbit_Stabiliser
[ok] Ordinal
[ok] Ordinals_and_Cardinals
[ok] Ordinary_Differential_Equations
[ok] PCF
[ok] PLM
[ok] POPLmark-deBruijn
[ok] PSemigroupsConvolution
[ok] Pairing_Heap
[ok] Paraconsistency
[ok] Parity_Game
[ok] Partial_Function_MR
[ok] Password_Authentication_Protocol
[ok] Perfect-Number-Thm
[ok] Perron_Frobenius
[ok] Pi_Calculus
[ok] Planarity_Certificates
[ok] Polynomial_Factorization
[ok] Polynomial_Interpolation
[ok] Polynomials
[ok] Pop_Refinement
[ok] Posix-Lexing
[ok] Possibilistic_Noninterference
[ok] Pratt_Certificate
[ok] Presburger-Automata
[ok] Prime_Harmonic_Series
[ok] Priority_Queue_Braun
[ok] Probabilistic_Noninterference
[ok] Probabilistic_System_Zoo
[ok] Probabilistic_While
[ok] Program-Conflict-Analysis
[ok] Promela
[ok] Proof_Strategy_Language
[ok] PropResPI
[ok] Propositional_Proof_Systems
[ok] Prpu_Maxflow
[ok] PseudoHoops
[ok] Psi_Calculi
[ok] Ptolemys_Theorem
[ok] QR_Decomposition
[ok] Quick_Sort_Cost
[ok] RIPEMD-160-SPARK
[ok] ROBDD
[ok] RSAPSS
[ok] Ramsey-Infinite
[ok] Random_BSTs
[ok] Random_Graph_Subgraph_Threshold
[ok] Randomised_Social_Choice
[ok] Rank_Nullity_Theorem
[ok] Real_Impl
[ok] Recursion-Theory-I
[ok] Refine_Imperative_HOL
[ok] Refine_Monadic
[ok] RefinementReactive
[ok] Regex_Equivalence
[ok] Regular-Sets
[ok] Regular_Algebras
[ok] Relation_Algebra
[ok] Rep_Fin_Groups
[ok] Residuated_Lattices
[ok] Resolution_FOL
[ok] Rewriting_Z
[ok] Ribbon_Proofs
[ok] Robbins-Conjecture
[ok] Root_Balanced_Tree
[ok] Routing
[ok] Roy_Floyd_Warshall
[ok] SATSolverVerification
[ok] SDS_Impossibility
[ok] SIFPL
[ok] SIFUM_Type_Systems
[ok] SPARCv8
[ok] Secondary_Sylow
[ok] Security_Protocol_Refinement
[ok] Selection_Heap_Sort
[ok] SenSocialChoice
[ok] Separata
[ok] Separation_Algebra
[ok] Separation_Logic_Imperative_HOL
[ok] SequentInvertibility
[ok] Shivers-CFA
[ok] ShortestPath
[ok] Show
[ok] Simpl
[ok] Simple_Firewall
[ok] Skew_Heap
[ok] Slicing
[ok] Sort_Encodings
[ok] Source_Coding_Theorem
[ok] Special_Function_Bounds
[ok] Splay_Tree
[ok] Sqrt_Babylonian
[ok] Stable_Matching
[ok] Statecharts
[ok] Stern_Brocot
[ok] Stewart_Apollonius
[ok] Stirling_Formula
[ok] Stone_Algebras
[ok] Stone_Kleene_Relation_Algebras
[ok] Stone_Relation_Algebras
[ok] Stream-Fusion
[ok] Stream_Fusion_Code
[ok] Strong_Security
[ok] Sturm_Sequences
[ok] Sturm_Tarski
[ok] Stuttering_Equivalence
[ok] Subresultants
[ok] SumSquares
[ok] SuperCalc
[ok] Surprise_Paradox
[ok] TLA
[ok] Tail_Recursive_Functions
[ok] Tarskis_Geometry
[ok] Timed_Automata
[ok] Topology
[ok] TortoiseHare
[ok] Transition_Systems_and_Automata
[ok] Transitive-Closure
[ok] Transitive-Closure-II
[ok] Tree-Automata
[ok] Tree_Decomposition
[ok] Triangle
[ok] Trie
[ok] Twelvefold_Way
[ok] Tycon
[ok] Types_Tableaus_and_Goedels_God
[ok] UPF
[ok] UPF_Firewall
[ok] UpDown_Scheme
[ok] Valuation
[ok] VectorSpace
[ok] Verified-Prover
[ok] Vickrey_Clarke_Groves
[ok] VolpanoSmith
[ok] WHATandWHERE_Security
[ok] Well_Quasi_Orders
[ok] Winding_Number_Eval
[ok] Word_Lib
[ok] WorkerWrapper
[ok] XML
[ok] Zeta_Function
[ok] pGCL