CBMC

swMATH9719MaRDI QIDQ21698

No author found.

Related Items (76)

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

This page was built for software: CBMC