Cordeiro, Lucas, Kesseli, Pascal, Kroening, Daniel, Schrammel, Peter and Trtik, Marek (2018) JBMC: a bounded model checking tool for verifying java bytecode. CAV 2018- 30th International Conference on Computer Aided Verification, Oxford, UK, July 14-17, 2018. Published in: CAV 2018 Computer Aided Verification. Springer, Cham. ISBN 9783319961446

	PDF - Accepted Version Download (382kB)
	PDF - Published Version Available under License Creative Commons Attribution. Download (598kB)

Abstract

We present a bounded model checking tool for verifying Java bytecode, which is built on top of the CPROVER framework, named Java Bounded Model Checker (JBMC). JBMC processes Java bytecode together with a model of the standard Java libraries and checks a set of desired properties. Experimental results show that JBMC can correctly verify a set of Java benchmarks from the literature and that it is competitive with two state-of-the-art Java verifiers.

Item Type:	Conference Proceedings
Keywords:	software verification, Java, bounded model checking, SAT solving
Schools and Departments:	School of Engineering and Informatics > Informatics
Subjects:	Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User:	Peter Schrammel
Date Deposited:	22 May 2018 09:06
Last Modified:	08 Nov 2018 10:00
URI:	http://sro.sussex.ac.uk/id/eprint/75980

View download statistics for this item

📧 Request an update