JBMC: a bounded model checking tool for verifying Java bytecode

JBMC: a bounded model checking tool for verifying Java bytecode

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 resul...

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí:	Cordeiro, L, Kesseli, P, Kroening, D, Schrammel, P, Trtik, M
Formáid:	Conference item
Foilsithe / Cruthaithe:	Springer, Cham 2018

Míreanna comhchosúla

Verifying information flow control in Java bytecodes
de réir: Mathewson, Nicholas A. (Nicholas Albert), 1977-
Foilsithe / Cruthaithe: (2014)

Incremental bounded model checking for embedded software
de réir: Schrammel, P, et al.
Foilsithe / Cruthaithe: (2017)

Selected tools for Java class and bytecode inspection in the educational environment
de réir: Dobravec Tomaž
Foilsithe / Cruthaithe: (2020-12-01)

JAVA BYTECODE INSTRUCTION USAGE COUNTING WITH ALGATOR
de réir: Tomaž DOBRAVEC
Foilsithe / Cruthaithe: (2019-01-01)

ESBMC-GPU A context-bounded model checking tool to verify CUDA programs
de réir: Monteiro, F, et al.
Foilsithe / Cruthaithe: (2017)

Applying Java bytecode static instrumentation for software dynamic analysis
de réir: S. P. Vartanov, et al.
Foilsithe / Cruthaithe: (2018-10-01)

Extracting and optimizing low-level bytecode from high-level verified Coq
de réir: Ioannidis, Eleftherios Ioannis.
Foilsithe / Cruthaithe: (2019)

Detecting Java Code Clones Based on Bytecode Sequence Alignment
de réir: Dongjin Yu, et al.
Foilsithe / Cruthaithe: (2019-01-01)

Refactoring Java Programs for Customizable Locks Based on Bytecode Transformation
de réir: Yang Zhang, et al.
Foilsithe / Cruthaithe: (2019-01-01)

SNITCH: Dynamic Dependent Information Flow Analysis for Independent Java Bytecode
de réir: Eduardo Geraldo, et al.
Foilsithe / Cruthaithe: (2019-08-01)

Computing Over−Approximations with Bounded Model Checking
de réir: Kroening, D
Foilsithe / Cruthaithe: (2006)

Computing over-approximations with bounded model checking
de réir: Kroening, D
Foilsithe / Cruthaithe: (2006)

Towards a General Framework for Formal Reasoning about Java Bytecode Transformation
de réir: Jean-Louis Lanet, et al.
Foilsithe / Cruthaithe: (2013-07-01)

Computational challenges in bounded model checking
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2005)

Completeness and Complexity of Bounded Model Checking
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2004)

Computational challenges in bounded model checking.
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2005)

Computational Challenges in Bounded Model Checking
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2015)

Verified software: theories, tools and experiments.
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2010)

Proving safety with trace automata and bounded model checking
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2015)

Linear Completeness Thresholds for Bounded Model Checking.
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2011)

Property-driven fence insertion using reorder bounded model checking
de réir: Joshi, S, et al.
Foilsithe / Cruthaithe: (2015)

Property-Driven Fence Insertion using Reorder Bounded Model Checking
de réir: Joshi, S, et al.
Foilsithe / Cruthaithe: (2015)

Towards automated bounded model checking of API implementations
de réir: Neville, D, et al.
Foilsithe / Cruthaithe: (2016)

A Complete Bounded Model Checking Algorithm for Pushdown Systems
de réir: Basler, G, et al.
Foilsithe / Cruthaithe: (2007)

Partial orders for efficient bounded model checking of concurrent software
de réir: Alglave, J, et al.
Foilsithe / Cruthaithe: (2013)

SJBCD: A Java Code Clone Detection Method Based on Bytecode Using Siamese Neural Network
de réir: Bangrui Wan, et al.
Foilsithe / Cruthaithe: (2023-08-01)

Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2003)

Verifying Digital Systems with MATLAB
de réir: Chaves, L, et al.
Foilsithe / Cruthaithe: (2017)

Bytecode-based approach for Ethereum smart contract classification
de réir: Dan LIN, et al.
Foilsithe / Cruthaithe: (2022-10-01)

Bytecode-based approach for Ethereum smart contract classification
de réir: Dan LIN, Kaixin LIN, Jiajing WU, Zibin ZHENG
Foilsithe / Cruthaithe: (2022-10-01)

Verifying digital systems with MATLAB
de réir: Chaves, L, et al.
Foilsithe / Cruthaithe: (2017)

Verifying Team Formation Protocols with Probabilistic Model Checking
de réir: Chen, T, et al.
Foilsithe / Cruthaithe: (2011)

Assisted coverage closure.
de réir: Nellis, A, et al.
Foilsithe / Cruthaithe: (2016)

Assisted coverage closure
de réir: Nellis, A, et al.
Foilsithe / Cruthaithe: (2016)

Verifying Patterns of Dynamic Architectures using Model Checking
de réir: Diego Marmsoler, et al.
Foilsithe / Cruthaithe: (2017-03-01)

Semi-Supervised Malware Clustering Based on the Weight of Bytecode and API
de réir: Yong Fang, et al.
Foilsithe / Cruthaithe: (2020-01-01)

A Tool for Checking ANSI−C Programs
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2004)

Verifying linearizability via optimized refinement checking
de réir: Dong, Jin Song, et al.
Foilsithe / Cruthaithe: (2013)

Mobile Code Anti-Reversing Scheme Based on Bytecode Trapping in ART
de réir: Geonbae Na, et al.
Foilsithe / Cruthaithe: (2019-06-01)

ScanAT: Identification of Bytecode-Only Smart Contracts With Multiple Attribute Tags
de réir: Yuntae Kim, et al.
Foilsithe / Cruthaithe: (2019-01-01)