SatAbs

swMATH12804MaRDI QIDQ24728FDOQ24728

Author name not available (Why is that?)

Cited In (36)

• Loop summarization using state and transition invariants
• Efficient strategies for CEGAR-based model checking
• Symbolic Counter Abstraction for Concurrent Software
• Counterexample guided path reduction for static program analysis
• Model-Checking HyperLTL for Pushdown Systems
• Computer Aided Verification
• Splitting via Interpolants
• Software model checking with explicit scheduler and symbolic threads
• Interpolation and model checking
• Predicate abstraction for program verification
• A model checking-based approach for security policy verification of mobile systems
• Automated formal analysis and verification: an overview
• Context-aware counter abstraction
• Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths
• Abstraction and abstraction refinement
• Verification and falsification of programs with loops using predicate abstraction
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Loop Summarization and Termination Analysis
• SAT-Based Model Checking
• Verification and refutation of probabilistic specifications via games
• Model checking boot code from AWS data centers
• Succinct representation of concurrent trace sets
• Abstraction Refinement of Linear Programs with Arrays
• Temporalization of Probabilistic Propositional Logic
• Automatic analysis of DMA races using model checking and \(k\)-induction
• Verification of Boolean programs with unbounded thread creation
• CPBPV: a constraint-programming framework for bounded program verification
• Leveraging compiler intermediate representation for multi- and cross-language verification
• Combining model checking and data-flow analysis
• Predicate Abstraction in Program Verification: Survey and Current Trends
• Tools and Algorithms for the Construction and Analysis of Systems
• Incremental false path elimination for static software analysis
• Verification of SpecC using predicate abstraction
• A Lightweight Approach for Loop Summarization
• Model checking of concurrent algorithms: from Java to C

This page was built for software: SatAbs