swMATH12804MaRDI QIDQ24728FDOQ24728
Author name not available (Why is that?)
Official website: http://link.springer.com/chapter/10.1007/978-3-540-31980-1_40
Cited In (94)
- Counterexample guided path reduction for static program analysis
- Software model checking with explicit scheduler and symbolic threads
- Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths
- Abstraction and abstraction refinement
- Succinct representation of concurrent trace sets
- Loop summarization using state and transition invariants
- Efficient strategies for CEGAR-based model checking
- Symbolic Counter Abstraction for Concurrent Software
- Model-Checking HyperLTL for Pushdown Systems
- Computer Aided Verification
- Splitting via Interpolants
- 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
- TopSpin
- Cogent
- FocusCheck
- CEGAR
- ARMC
- SCRATCH
- Princess
- Goanna
- bv2epr
- Cseq
- CPAchecker
- Predator
- ComFoRT
- SymmSpin
- 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
- UFO
- ACL2s
- Augur 2
- Bebop
- Cellss
- SPEED
- CBMC
- CVT
- SLAB
- Orion
- RacerX
- SCOOT
- MOPS
- TVLA
- Threader
- TLPVS
- Goldilocks
- FOCI
- MoonWalker
- CSSV
- Joogie
- Lazy-CSeq
- MAGIC
- Loop Summarization and Termination Analysis
- LusSy
- Wolverine
- Aglets
- Coverity
- DDVerify
- VS3
- EUREKA
- Ultimate Kojak
- ANaConDA
- CPAlien
- FrankenBit
- Jakstab
- MU-CSeq
- Symbiotic 2
- Klocwork
- Kotlin
- Calysto
- Cascade
- CIVL
- GraVy
- Pyston
- SAT-Based Model Checking
- Verification and refutation of probabilistic specifications via games
- Model checking boot code from AWS data centers
- 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
