Archive of Formal Proofs

Test status of entries in the AFP development version

Isabelle revision:	c05bec5d01ad
AFP revision:	fd20a4c244d8
Build time:	Tue, 18 Apr 2017 08:10:09 GMT
Build URL:	Jenkins
Job name:	afp-repo-afp

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