SatAbs
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Model checking of concurrent algorithms: from Java to C
- 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
- Splitting via Interpolants
- Computer Aided Verification
- Software model checking with explicit scheduler and symbolic threads
- Interpolation and model checking
- A model checking-based approach for security policy verification of mobile systems
- Predicate abstraction for program verification
- 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
- CPBPV
- TopSpin
- Cogent
- FocusCheck
- Zing
- DiVer
- StEAM
- ACSAR
- BLAST
- SLAM
- CEGAR
- ARMC
- SCRATCH
- Princess
- Goanna
- bv2epr
- Cseq
- CPAchecker
- Predator
- ComFoRT
- SymmSpin
- 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
- LusSy
- Wolverine
- Aglets
- Coverity
- DDVerify
- VS3
- EUREKA
- Ultimate Kojak
- ANaConDA
- CPAlien
- FrankenBit
- Jakstab
- MU-CSeq
- Symbiotic 2
- Klocwork
- Kotlin
- Calysto
- Cascade
- CIVL
- GraVy
- Pyston
- Abstraction and abstraction refinement
- Verification and falsification of programs with loops using predicate abstraction
- Loop Summarization and Termination Analysis
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- SAT-Based Model Checking
- Model checking boot code from AWS data centers
- Verification and refutation of probabilistic specifications via games
- Succinct representation of concurrent trace sets
- Automatic analysis of DMA races using model checking and k-induction
- Abstraction Refinement of Linear Programs with Arrays
- Temporalization of Probabilistic Propositional Logic
- CPBPV: a constraint-programming framework for bounded program verification
- Verification of Boolean programs with unbounded thread creation
- 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
- Incremental false path elimination for static software analysis
- Tools and Algorithms for the Construction and Analysis of Systems
- Verification of SpecC using predicate abstraction
This page was built for software: SatAbs
