CBMC

swMATH9719MaRDI QIDQ21698FDOQ21698

Author name not available (Why is that?)

Cited In (76)

• Loop summarization using state and transition invariants
• Finding and fixing faults
• Efficient SAT-based bounded model checking for software verification
• Verifying Whiley programs with Boogie
• Combining Model Checking and Data-Flow Analysis
• Translating Xd-C programs to MSVL programs
• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
• Not all bugs are created equal, but robust reachability can tell the difference
• Quantifying software reliability via model-counting
• Verified cryptographic code for everybody
• Loop Summarization Using Abstract Transformers
• Satisfiability Checking: Theory and Applications
• SATenstein: automatically building local search SAT solvers from components
• Exploiting binary floating-point representations for constraint propagation
• Tools and Algorithms for the Construction and Analysis of Systems
• Symbolic computation via program transformation
• Scalable and precise refinement of cache timing analysis via path-sensitive verification
• On black-box optimization in divide-and-conquer SAT solving
• Fairness modulo theory: a new approach to LTL software model checking
• Symbolic predictive analysis for concurrent programs
• An extension of lazy abstraction with interpolation for programs with arrays
• Deciding floating-point logic with abstract conflict driven clause learning
• A formal methods approach to predicting new features of the eukaryotic vesicle traffic system
• Verification by gambling on program slices
• Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
• Under-approximating loops in C programs for fast counterexample detection
• A bounded model checker for three-valued abstractions of concurrent software systems
• Efficient bounded model checking of heap-manipulating programs using tight field bounds
• Matching Multiplications in Bit-Vector Formulas
• Automated formal synthesis of provably safe digital controllers for continuous plants
• LCTD: test-guided proofs for C programs on LLVM
• From non-preemptive to preemptive scheduling using synchronization synthesis
• DSValidator
• SAT-Based Model Checking
• Inductive benchmarks for automated reasoning
• Budget-bounded model-checking pushdown systems
• Model checking boot code from AWS data centers
• Information Theory and Security: Quantitative Information Flow
• Automatic analysis of DMA races using model checking and \(k\)-induction
• Doomed program points
• Incremental bounded model checking for embedded software
• Mutation-Based Test Case Generation for Simulink Models
• CPBPV: a constraint-programming framework for bounded program verification
• Data compression for proof replay
• Title not available (Why is that?)
• Automatically verifying temporal properties of pointer programs with cyclic proof
• The configurable SAT solver challenge (CSSC)
• Partitioned Memory Models for Program Analysis
• On compiling Boolean circuits optimized for secure multi-party computation
• Why does Astrée scale up?
• Sharpening constraint programming approaches for bit-vector theory
• A unifying view on SMT-based software verification
• VST-Floyd: a separation logic tool to verify correctness of C programs
• A compiler for MSVL and its applications
• SMT-based model checking for recursive programs
• The \textsc{MergeSat} solver
• Verification of Concurrent Programs on Weak Memory Models
• URSA: A System for Uniform Reduction to SAT
• Empirical software metrics for benchmarking of verification tools
• Abstract semantic diffing of evolving concurrent programs
• A taxonomy of exact methods for partial Max-SAT
• An automatic method for the dynamic construction of abstractions of states of a formal model
• Compositional Sequentialization of Periodic Programs
• Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications
• Applying Software Model Checking Techniques for Behavioral UML Models
• Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic
• A compositional behavioral modeling framework for embedded system design and conformance checking
• Embedded software verification using symbolic execution and uninterpreted functions
• Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)
• Sequentialization Using Timestamps
• Transfer Function Synthesis without Quantifier Elimination
• Transfer of Model Checking to Industrial Practice
• Shape Neutral Analysis of Graph-based Data-structures
• System-level state equality detection for the formal dynamic verification of legacy distributed applications
• Verifying a scheduling protocol of safety-critical systems
• Transfer function synthesis without quantifier elimination

This page was built for software: CBMC