Deductive Verification of Concurrent Programs and its Application to Secure Information Flow for Java

@phdthesis{Grahl15,
  author	= {Daniel Grahl},
  title		= {Deductive Verification of Concurrent Programs and its
		   Application to Secure Information Flow for {Java}},
  school	= {Karlsruhe Institute of Technology},
  year		= {2015},
  month		= oct,
  url		= {https://publikationen.bibliothek.kit.edu/1000050695},
  urn		= {urn:nbn:de:swb:90-506951},
  doi		= {10.5445/IR/1000050695},
  license	= {https://creativecommons.org/licenses/by-sa/4.0},
  abstract	= {The goal of this thesis is to develop a rigorous analysis
		   technique for proving functional and relational correctness
		   of shared-memory multi-threaded object-oriented software
		   systems---such as programs written in the Java
		   language---based on formal program semantics and deductive
		   verification. This work contains the first approach towards
		   a semantically precise information flow anlaysis for
		   concurrent programs.}
}