#
# List most important files first!
#

# "Getting Started"
standard_key/prop_log/contraposition.txt
standard_key/prop_log/liarsville.txt
firstTouch/01-Agatha/README.txt
firstTouch/02-Subset/README.txt
# removed duplicate directory!
# firstTouch/03-SumAndMax/README.txt
heap/vstte10_01_SumAndMax/FIRSTTOUCH.txt
# moved to competitions below
# firstTouch/04-LinkedList/README.txt
# 05 seems to be broken ... deactivated ... revived
firstTouch/06-BinarySearch/README.txt
firstTouch/08-Java5/README.txt
heap/removeDups/README.txt
firstTouch/09-Quicktour/README.txt
firstTouch/10-SITA/README.txt
firstTouch/11-StateMerging/README.txt

# The KeY Book (note: the comments here are only for maintainability, if you want to move an entry to a different section, look into the individual txt file!)
## Chapter 15 - Using the KeY Prover
newBook/Using_KeY/Building_Propositional_Proofs/README.txt
newBook/Using_KeY/Building_First-Order_Proofs/README.txt
newBook/Using_KeY/Building_Dynamic_Logic_Proofs/01-exchange/README.txt
newBook/Using_KeY/Building_Dynamic_Logic_Proofs/02-executeByProving/README.txt
newBook/Using_KeY/Building_Dynamic_Logic_Proofs/09-methodCall/README.txt
newBook/Using_KeY/Building_Dynamic_Logic_Proofs/09-methodCall/README2.txt
newBook/Using_KeY/Building_Dynamic_Logic_Proofs/03-updates/README.txt
newBook/Using_KeY/Building_Dynamic_Logic_Proofs/04-activeStmt/README.txt
newBook/Using_KeY/Building_Dynamic_Logic_Proofs/05-symbolicExecution/README.txt
newBook/Using_KeY/Building_Dynamic_Logic_Proofs/06-postIncrement/README.txt
newBook/Using_KeY/Building_Dynamic_Logic_Proofs/07-quantifyProgVals/README.txt
newBook/Using_KeY/Building_Dynamic_Logic_Proofs/08-postIncrNoUpdate/README.txt
newBook/Using_KeY/Understanding_Proof_Situations/README.txt
newBook/Using_KeY/Further-Features/README.txt
## Chapter 16 - Formal Verification with KeY: A Tutorial
newBook/Chapter_16/PostInc/README.txt
newBook/Chapter_16/Sort/README.txt
newBook/Chapter_16/SortPerm/README.txt

# Algorithms
firstTouch/05-ReverseArray/README.txt
heap/saddleback_search/README.txt
heap/permutedSum/README.txt
heap/quicksort/README.txt
heap/BoyerMoore/README.txt

# Dynamic Frames
## Block & Loop Contracts
heap/block_loop_contracts/Simple/README.txt
heap/block_loop_contracts/Divide/README.txt
heap/block_loop_contracts/InternalExternal/README.txt
heap/block_loop_contracts/List/README.txt
#
heap/SmansEtAl/README.txt
heap/Transactions/README.txt
heap/list/README.txt
heap/list_ghost/README.txt
heap/list_seq/README.txt
heap/observer/README.txt
#heap/simple/README.txt

# Benchmarks
## VSComp 10
heap/vstte10_01_SumAndMax/README.txt
heap/vstte10_02_Invert/README.txt
heap/vstte10_03_LinkedList/README.txt
heap/vstte10_04_Queens/README.txt
heap/vstte10_05_Queue/README.txt
## VerifyThis2011
heap/verifyThis11_1_Maximum/README.txt
## FM12
heap/fm12_01_LRS/README.txt
## VerifyThis2015
heap/verifyThis15_1_RelaxedPrefix/README.txt
heap/verifyThis15_2_ParallelGcd/README.txt
heap/verifyThis15_3_DLL/README.txt
## VerifyThis2017
heap/verifyThis17_1_PairInsertionSort/README.txt
## VACID-0
heap/vacid0_01_SparseArray/README.txt
# Red-Black-Trees cannot be parsed currently
# heap/vacid0_05_RedBlackTrees/README.txt
## WeideEtAl
heap/WeideEtAl_01_AddAndMultiply/README.txt
heap/WeideEtAl_02_BinarySearch/README.txt

# Information Flow
heap/information_flow/README-ArrayList.txt
InformationFlow/MiniExamples/README.txt
InformationFlow/Sum/README.txt
InformationFlow/MethodContracts/README.txt
InformationFlow/ToyVoting/README.txt
InformationFlow/SimpleEvoting/README.txt
InformationFlow/ToyBanking/README.txt
InformationFlow/ToyBanking/README2.txt
InformationFlow/NewObjects/README.txt
InformationFlow/LoopInvariants/README.txt
InformationFlow/BlockContracts/README.txt
