ETAPS 2019 (series) / Poster session /
JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)
Sat 6 Apr 2019 15:16 - 15:38 at Coffee area (Posters) - Workshop Poster Exhibition (Saturday) Chair(s): Jan Kofroň
Sun 7 Apr 2019 11:58 - 12:20 at Coffee area (Posters) - Workshop Poster Exhibition (Sunday)
Mon 8 Apr 2019 20:08 - 20:12 at 1st Floor Reception Area (Posters) - Main Poster Session Chair(s): Konrad Siek
Sun 7 Apr 2019 11:58 - 12:20 at Coffee area (Posters) - Workshop Poster Exhibition (Sunday)
Mon 8 Apr 2019 20:08 - 20:12 at 1st Floor Reception Area (Posters) - Main Poster Session Chair(s): Konrad Siek
JBMC is a bounded model checking tool for verifying Java bytecode. It is built on top of the CPROVER framework. JBMC processes Java bytecode together with a model of the standard Java libraries. It checks a set of desired properties, such as assertions and absence of uncaught exceptions, under given bounds on loops, recursion and data structures. Internally, it uses the same bounded model checking engine as its sibling tool CBMC and discharges the generated verification conditions with the help of MiniSAT 2.2.1.
Sat 6 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sat 6 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 7 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 7 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 8 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 8 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change