Efficient SAT-based bounded model checking for software verification

No abstract is available for this paper.

• Publication year

  2008

• Venue

  Theoretical Computer Science

• Publication date

  2008-09-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1016/j.tcs.2008.03.013
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Model checking

  2009cited by this paper
• Disjunctive image computation for software verification

  2007cited by this paper
• Program Analysis Using Symbolic Ranges

  2007cited by this paper
• Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop

  2006cited by this paper
• Efficient Strongly Relational Polyhedral Analysis

  2006cited by this paper
• Mixed symbolic representations for model checking software programs

  2006cited by this paper
• Static Analysis of Numerical Algorithms

  2006cited by this paper
• Static Analysis in Disjunctive Numerical Domains

  2006cited by this paper
• Disjunctive Image Computation for Embedded Software Verification

  2006cited by this paper
• Localization and Register Sharing for Predicate Abstraction

  2005cited by this paper
• Model checking C programs using F-Soft

  2005cited by this paper
• F-Soft: Software Verification Platform

  2005cited by this paper
• DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems

  2005cited by this paper
• A survey of recent advances in SAT-based formal verification

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

  2004cited by this paper
• The octahedron abstract domain

  2004cited by this paper
• Predicate Abstraction of ANSI-C Programs Using SAT

  2004cited by this paper
• Verification of proofs of unsatisfiability for CNF formulas

  2003cited by this paper
• Interpolation and SAT-Based Model Checking

  2003cited by this paper
• Bogor: an extensible and highly-modular software model checking framework

  2003cited by this paper
• Iterative abstraction using SAT-based BMC with proof analysis

  2003cited by this paper
• Behavioral consistency of C and Verilog programs using bounded model checking

  2003cited by this paper
• CSSV: towards a realistic tool for statically detecting all buffer overflows in C

  2003cited by this paper
• Efficient distributed SAT and SAT-based distributed Bounded Model Checking

  2003cited by this paper
• Automatic Abstraction without Counterexamples

  2003cited by this paper
• A Symbolic Approach to Predicate Abstraction

  2003cited by this paper
• Context-sensitive slicing of concurrent programs

  2003cited by this paper
• Abstraction and BDDs Complement SAT-Based BMC in DiVer

  2003influential reference
• Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications

  2003cited by this paper
• Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis

  2002cited by this paper
• Applying SAT Methods in Unbounded Symbolic Model Checking

  2002cited by this paper
• BerkMin: A fast and robust SAT-solver

  2002cited by this paper
• Efficient Computation of Recurrence Diameters

  2002cited by this paper
• Lazy abstraction

  2002cited by this paper
• Program slicing for VHDL

  2002cited by this paper
• Pointer analysis: haven't we solved this problem yet?

  2001cited by this paper
• Chaff: engineering an efficient SAT solver

  2001cited by this paper
• The octagon abstract domain

  2001cited by this paper
• Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering : PASTE '01, Snowbird, Utah, USA, June 18-19, 2001

  2001cited by this paper
• Verifying Network Protocol Implementations by Symbolic Refinement Checking

  2001influential reference
• A New Numerical Abstract Domain Based on Difference-Bound Matrices

  2001cited by this paper
• jMocha: a model checking tool that exploits design structure

  2001cited by this paper
• Symbolic bounds analysis of pointers, array indices, and accessed memory regions

  2000cited by this paper
• SAT-Based Image Computation with Application in Reachability Analysis

  2000cited by this paper
• A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities

  2000cited by this paper
• Model checking programs

  2000cited by this paper
• ABCD: eliminating array bounds checks on demand

  2000cited by this paper
• Counterexample-Guided Abstraction Refinement

  2000cited by this paper
• Bandera: extracting finite-state models from Java source code

  2000cited by this paper
• Checking Safety Properties Using Induction and a SAT-Solver

  2000cited by this paper
• Bebop: A Symbolic Model Checker for Boolean Programs

  2000cited by this paper
• Model checking JAVA programs using JAVA PathFinder

  2000cited by this paper
• Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results

  1999cited by this paper
• Experience with Predicate Abstraction

  1999cited by this paper
• Symbolic model checking using SAT procedures instead of BDDs

  1999cited by this paper
• GRASP: A Search Algorithm for Propositional Satisfiability

  1999cited by this paper
• SpC: synthesis of pointers in C application of pointer analysis to the behavioral synthesis from C

  1998cited by this paper
• The Model Checker SPIN

  1997cited by this paper
• VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software

  1997cited by this paper
• Reachability Analysis of Pushdown Automata: Application to Model-Checking

  1997cited by this paper
• Construction of Abstract State Graphs with PVS

  1997cited by this paper
• CADP - A Protocol Validation and Verification Toolbox

  1996cited by this paper
• Accurate static branch prediction by value range propagation

  1995cited by this paper
• A survey of program slicing techniques

  1994cited by this paper
• Symbolic Model Checking

  1993cited by this paper
• Model-Checking in Dense Real-time

  1993cited by this paper
• Imperative functional programming

  1993cited by this paper
• Symbolic model checking

  1992cited by this paper
• Graph-based Algorithm for Boolean Function Manipulation

  1989cited by this paper
• Reasoning about Networks with Many Identical Finite State Processes

  1989cited by this paper
• Automatic discovery of linear restraints among variables of a program

  1978cited by this paper
• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

  1977cited by this paper
• Static determination of dynamic properties of programs

  1976cited by this paper
• Affine relationships among variables of a program

  1976cited by this paper

• MHQ-SAT: An End-to-End SAT Solver with a Multi-Head Hierarchical Query Mechanism

  2026cites this paper
• Kissat_MAB_CoRephase: Combining Different Rephasing Heuristics Using MAB in SAT

  2025cites this paper
• SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation

  2025cites this paper
• Quantum software engineering and potential of quantum computing in software engineering research: a review

  2025cites this paper
• Reward Defining in Multi-armed Bandit SAT Strategy

  2025cites this paper
• Structure based SAT dataset for analysing GNN generalisation

  2025cites this paper
• Higher order Weighted Random k Satisfiability ($k = 1, 3$) in Discrete Hopfield Neural Network

  2025cites this paper
• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem

  2024cites this paper
• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection

  2024cites this paper
• Augmented Electronic Ising Machine as an Effective SAT Solver

  2023cites this paper
• Verified Encodings for SAT Solvers

  2023cites this paper
• A Bloom Filter-based Algorithm for Fast Detection of Common Variables

  2023cites this paper
• Comparing the hardness of MAX 2-SAT problem instances for quantum and classical algorithms

  2022cites this paper
• Solving dependency quantified Boolean formulas using quantifier localization

  2022cites this paper
• NSNet: A General Neural Probabilistic Framework for Satisfiability Problems

  2022cites this paper
• Migrating Solver State

  2022cites this paper
• Backtracking (the) Algorithms on the Hamiltonian Cycle Problem

  2021cites this paper
• On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers

  2020cites this paper
• Sensitivity Analysis of Locked Circuits

  2020cites this paper
• in Computing

  2020cites this paper
• Modeling Techniques for Logic Locking

  2020cites this paper
• Evaluation of Program Slicing in Software Verification

  2019cites this paper
• Localizing Quantifiers for DQBF

  2019cites this paper
• On CDCL-Based Proof Systems with the Ordered Decision Strategy

  2019cites this paper
• Chasing Minimal Inductive Validity Cores in Hardware Model Checking

  2019cites this paper
• A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving

  2019cites this paper
• Quantifier Localization for DQBF

  2019cites this paper
• Strong Extension-Free Proof Systems

  2019cites this paper
• A Proof System for a Unified Temporal Logic

  2019cites this paper
• The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation

  2019cites this paper
• Automatically verifying temporal properties of heap programs with cyclic proof

  2019cites this paper
• CDCL SAT Solvers, Subsystems of Resolution, and the Ordered Decision Strategy

  2019cites this paper
• An Efficient SAT-Based Test Generation Algorithm with GPU Accelerator

  2018cites this paper
• Chapter Two - Advances in Software Model Checking

  2018cites this paper
• Model checking boot code from AWS data centers

  2018cites this paper
• SAT Solving with distributed local search

  2018cites this paper
• SAT-Based Synthesis of Spoofing Attacks in Cyber-Physical Control Systems

  2018cites this paper
• Analysis of Incomplete Circuits Using Dependency Quantified Boolean Formulas

  2018cites this paper
• A Predictive Data Analytic for the Hardness of Hamiltonian Cycle Problem Instances

  2018cites this paper
• Assembly program verification for multiprocessors with relaxed memory model using SMT solver

  2017cites this paper
• Computing properties of stable configurations of thermodynamic binding networks

  2017cites this paper
• Design, implementation and evaluation of a distributed CDCL framework

  2017cites this paper
• Formal Verification of Firmware-Based System-on-Chip Modules

  2017cites this paper
• Enforcement in Abstract Argumentation via Boolean Optimization

  2017cites this paper
• Normal Form of n-Valued Lukasiewicz Logic Formulas

  2017cites this paper
• Short Proofs Without New Variables

  2017cites this paper
• The science of brute force

  2017cites this paper
• Skolem Functions for DQBF

  2016cites this paper
• Efficient Certified RAT Verification

  2016cites this paper
• Dependency Schemes for DQBF

  2016cites this paper
• Solving DQBF through quantifier elimination

  2015cites this paper
• Solving DQBF Through Quantifier Elimination by Karina Gitina

  2015cites this paper
• AVACS – Automatic Verification and Analysis of Complex Systems REPORTS of SFB / TR 14 AVACS

  2015cites this paper
• Flexible SAT-based framework for incremental bounded upgrade checking

  2015cites this paper
• Automated incremental software verification

  2015cites this paper
• Symbolic Detection of Assertion Dependencies for Bounded Model Checking

  2015cites this paper
• FPGA Acceleration of Decision-Based Problems using Heterogeneous Computing

  2014cites this paper
• Intelligent Management of Inter-Thread Synchronization Dependencies for Concurrent Programs

  2014cites this paper
• Scalable and scope-bounded software verification in Varvel

  2014cites this paper
• Incremental bounded software model checking

  2014cites this paper
• Controllability for discrete event systems modelled in VeriJ

  2014cites this paper
• Simulation DNA Algorithm

  2014cites this paper
• Behavioral modeling and formal verification of a resource discovery approach in Grid computing

  2014cites this paper
• Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection

  2014cites this paper
• The bounded model checker LLBMC

  2013influential citation
• LLVMVF: A Generic Approach for Verification of Multicore Software

  2013cites this paper
• Constructing Software Structure Graph through Progressive Execution

  2013cites this paper
• Resource Constrained Project Scheduling with General Precedence Relations Optimized with SAT

  2013cites this paper
• Accelerating Software Model Checking Based on Program Backbone

  2013cites this paper
• Progress in Artificial Intelligence

  2013cites this paper
• A New Formal Verification Approach for Hardware-dependent Embedded System Software

  2013cites this paper
• An equivalence checker for hardware-dependent embedded system software

  2013cites this paper
• A computational model for SAT-based verification of hardware-dependent low-level embedded system software

  2013cites this paper
• LLBMC: Improved Bounded Model Checking of C Programs Using LLVM - (Competition Contribution)

  2013cites this paper
• Practical lock/unlock pairing for concurrent programs

  2013cites this paper
• LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation - (Competition Contribution)

  2012cites this paper
• Predicate Abstraction with Block Abstraction Memoization ∗ ( Technical Report )

  2012cites this paper
• MEMICS - Memory Interval Constraint Solving of (concurrent) Machine Code

  2012cites this paper
• Hardware/software formal co-verification using hardware verification techniques

  2012cites this paper
• LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR

  2012cites this paper
• Predicate Analysis with Block-Abstraction Memoization

  2012cites this paper
• Marcelo André Barbosa de Sousa A Framework for Formal Verification of Concurrent Software

  2012cites this paper
• High-Level Verification

  2011cites this paper
• SLAM is a program-analysis engine used to check if clients of an API follow the API ’ s stateful usage rules

  2011cites this paper
• A decade of software model checking with SLAM

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

  2010cites this paper
• SAT Solving with Reference Points

  2010cites this paper
• The Edge of Graph Transformation - Graphs for Behavioural Specification

  2010cites this paper
• Program analysis with interpolants

  2010cites this paper
• SAT Solvers for Queries over Tree Automata with Constraints

  2010cites this paper
• Propelling SAT and SAT-based BMC using careset

  2010influential citation
• Parallelizing MiniSat

  2010cites this paper
• Dynamic Path Reduction for Software Model Checking

  2009cites this paper
• Model checking sequential software programs via mixed symbolic analysis

  2009cites this paper
• Software model checking

  2009cites this paper
• CPBPV: a constraint-programming framework for bounded program verification

  2008cites this paper
• Efficient Modeling of Concurrent Systems in BMC

  2008cites this paper
• Improving Encoding Efficiency for Bounded Model Checking

  2008cites this paper
• Disjunctive image computation for software verification

  2007cites this paper
• Using Bounded Model Checking with BOGOR

  2007cites this paper