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

PhD Thesis

Author(s):Daniel Grahl
School:Karlsruhe Institute of Technology
Year:2015
URL:http://digbib.ubka.uni-karlsruhe.de/volltexte/1000050695
DOI:10.5445/IR/1000050695

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.

BibTeX

@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		= {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000050695},
  urn		= {urn:nbn:de:swb:90-506951},
  doi		= {10.5445/IR/1000050695},
  license	= {http://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.}
}