*Result*: Capturing program models with BISM
Title:
Capturing program models with BISM
Authors:
Contributors:
Compiler Optimization and Run-time Systems (CORSE), Centre Inria de l'Université Grenoble Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG), Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP), Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP), Université Grenoble Alpes (UGA)
Source:
SAC 2022 - 37th ACM Symposium on Applied Computing - Software Verification and Testing Track ; https://inria.hal.science/hal-03911682 ; SAC 2022 - 37th ACM Symposium on Applied Computing - Software Verification and Testing Track, Apr 2022, Brno (Virtuel), Czech Republic. ⟨10.1145/3477314.3507239⟩
Publisher Information:
CCSD
Publication Year:
2022
Collection:
Université Grenoble Alpes: HAL
Subject Terms:
Runtime Verification Typestate Analysis Parametric Monitoring Instrumentation Java Bytecode Control Flow, Runtime Verification, Typestate Analysis, Parametric Monitoring, Instrumentation, Java Bytecode, Control Flow, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]
Subject Geographic:
Document Type:
*Conference*
conference object
Language:
English
DOI:
10.1145/3477314.3507239
Availability:
Rights:
info:eu-repo/semantics/OpenAccess
Accession Number:
edsbas.9562E244
Database:
BASE
*Further Information*
*International audience ; In this paper, we present an extension of the Java bytecode instrumentation tool BISM that captures and prepares a model that abstracts the program behavior at the intra-procedural level. We analyze program methods we are interested in monitoring and construct a control-flow graph automaton where the states represent actions of the program that produce events. Directed towards monitoring general behavioral properties at runtime, the resulting model is presented for the users to write static analyzers and combine both static and runtime verification.*