ID	Type	Status	Priority	Milestone	Owner		Summary + Labels	...
	6	Enhancement	Accepted	Low	----	----		PLURAL: Warn user that they need frame permission to change state
	12	Enhancement	Assigned	Low	----	nels.beckman		Check initializers of static fields
	13	Enhancement	Assigned	Low	----	nels.beckman		For immutable permissions, make state guarantees and stateInfo interchangable.
	15	Defect	Started	Medium	----	kevin.bierhoff		Lattice comparison and join issues
	16	Defect	Assigned	Medium	----	kevin.bierhoff		releasedFrom attribute is ignored
	17	Defect	Assigned	Medium	----	kevin.bierhoff		Unpacking does not purify invariants above root node
	18	Defect	Assigned	Medium	----	kevin.bierhoff		Field read/assignment checks are not sufficient
	21	Enhancement	Assigned	Low	----	nels.beckman		Default permissions for un-annotated fields and methods
	23	Enhancement	Started	Medium	----	kevin.bierhoff		Better local alias analysis
	24	Enhancement	Assigned	Low	----	kevin.bierhoff		Linear connectives in method pre- and post-conditions, and in invariants
	25	Enhancement	Assigned	Medium	----	kevin.bierhoff		More flexible implication syntax, and support in invariants and methods   Usability
	26	Enhancement	Assigned	Medium	----	kevin.bierhoff		Check @Param and @Release in method implementations; track parameters through invariants
	27	Enhancement	Assigned	Low	----	kevin.bierhoff		Check that marker states are indeed fixed through the object lifetime
	28	Enhancement	Assigned	Low	----	kevin.bierhoff		Default field values for not explicitly initialized fields
	29	Enhancement	Assigned	Low	----	kevin.bierhoff		Access inherited fields and fields of other objects than the reciever   Usability
	30	Enhancement	Assigned	Medium	----	kevin.bierhoff		Reduce context fanout during packing / unpacking   Performance
	31	Enhancement	Assigned	Medium	----	kevin.bierhoff		Keep track of named fraction instantiations   Performance
	32	Enhancement	Started	Medium	----	kevin.bierhoff		Fraction statisfiability speedups   Performance
	33	Enhancement	Assigned	Medium	----	kevin.bierhoff		Implicit method parameters   Usability
	34	Enhancement	Assigned	Medium	----	nels.beckman		Handling lists and arrays   Usability
	35	Enhancement	Started	Medium	----	kevin.bierhoff		Borrowing annotation for getter result   Usability
	37	Enhancement	Assigned	Medium	----	kevin.bierhoff		Flagging impossible code and unnecessary tests   Usability
	38	Enhancement	Assigned	Low	----	nels.beckman		Array bounds checks and integer tracking
	39	Enhancement	Assigned	Low	----	kevin.bierhoff		Default null checks (optional)
	40	Enhancement	Assigned	Low	----	kevin.bierhoff		Correlated ifs
	41	Enhancement	Assigned	Low	----	kevin.bierhoff		Use exceptions / regular returns (also null etc.) to indicate states or even permissions
	42	Enhancement	Assigned	Low	----	kevin.bierhoff		Reference equality invariants / method pre-/post-conditions
	45	Defect	New	Medium	----	nels.beckman		dynamic state logic join too conservative
	67	Defect	Accepted	Medium	----	nels.beckman		Fiddle: Dynamic State Tests are not illustrated
	70	Defect	New	High	----	nels.beckman		Field permission is lost when method argument contains method call
	73	Defect	New	Medium	----	----		Infinite loop triggered in Plural/Crystal by defining an "alive" class state on an object