LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation - (Competition Contribution)

No abstract is available for this paper.

• Publication year

  2012

• Venue

  International Conference on Tools and Algorithms for Construction and Analysis of Systems

• Publication date

  2012-03-24

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/978-3-642-28756-5_44
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR

  2012cited by this paper
• A Theory of C-Style Memory Allocation ?

  2011cited by this paper
• A Precise Memory Model for Low-Level Bounded Model Checking

  2010cited by this paper
• Efficient SAT-based bounded model checking for software verification

  2008cited by this paper
• A Decision Procedure for Bit-Vectors and Arrays

  2007cited by this paper
• LLVM: a compilation framework for lifelong program analysis & transformation

  2004influential reference
• A Temporal Logic of Nested Calls and Returns

  2004cited by this paper
• A Tool for Checking ANSI-C Programs

  2004cited by this paper

• Verifying Fortran Programs with CIVL

  2022cites this paper
• Formal fault injection vulnerability detection in binaries : a software process and hardware validation. (Détection formelle de vulnérabilité créée par injection de faute au niveau binaire : un processus logiciel et une validation matérielle)

  2019cites this paper
• Verification of Safety Functions Implemented in Rust - a Symbolic Execution based approach

  2019cites this paper
• Compiling C and C++ Programs for Dynamic White-Box Analysis

  2019cites this paper
• Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems

  2018cites this paper
• A Unifying View on SMT-Based Software Verification

  2017cites this paper
• An Automated Formal Process for Detecting Fault Injection Vulnerabilities in Binaries and Case Study on PRESENT

  2017cites this paper
• Using Off-the-Shelf Exception Support Components in C++ Verification

  2017cites this paper
• An automated and scalable formal process for detecting fault injection vulnerabilities in binaries

  2017cites this paper
• Verified Software. Theories, Tools, and Experiments

  2016cites this paper
• MLSA: A static bugs analysis tool based on LLVM IR

  2016cites this paper
• SMT-based Software Model Checking: An Experimental Comparison of Four Algorithms

  2016cites this paper
• Model Checking and Model-Based Testing: Improving Their Feasibility by Lazy Techniques, Parallelization, and Other Optimizations

  2016cites this paper
• Theory and Implementation of Software Bounded Model Checking

  2016cites this paper
• LLVM Transformations for Model Checking

  2016cites this paper
• Symbolic Crosschecking of Data-Parallel Floating-Point Code

  2014cites this paper
• Improving C++ Software Quality with Static Code Analysis

  2014influential citation
• The bounded model checker LLBMC

  2013cites this paper
• Combined WCET analysis of bitcode and machine code using control-flow relation graphs

  2013cites this paper
• Here be wyverns ! Verifying LLVM bitcode with llStar

  2013cites this paper
• Построение спецификаций программных интерфейсов в открытой системе покомпонентной верификации ядра Linux

  2013cites this paper
• A Theory of Arrays with set and copy Operations

  2013cites this paper
• Static Verification Tools for C Programs and Linux Device Drivers: A Survey

  2012cites this paper
• Competition on Software Verification - (SV-COMP)

  2012cites this paper
• Обзор инструментов статической верификации Си программ в применении к драйверам устройств операционной системы Linux

  2012cites this paper
• Linux Driver Verification - (Position Paper)

  2012cites this paper