veriSoft
From MaRDI portal
VeriSoft
Cited in
(only showing first 100 items - show all)- Dynamic Path Reduction for Software Model Checking
- State Space Reduction of Rewrite Theories Using Invisible Transitions
- Syntax-directed model checking of sequential programs
- Delay-bounded scheduling without delay!
- Stateless model checking under a reads-value-from equivalence
- scientific article; zbMATH DE number 1863177 (Why is no real title available?)
- scientific article; zbMATH DE number 1903350 (Why is no real title available?)
- Model checking concurrent programs
- Effective Program Verification for Relaxed Memory Models
- A formally verified compiler back-end
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Balancing the load. Leveraging a semantics stack for systems verification
- Formal memory models for the verification of low-level operating-system code
- Model checking dynamic memory allocation in operating systems
- Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions
- Model Checking Software
- Proving the correctness of client/server software
- Tools and Algorithms for the Construction and Analysis of Systems
- Software model checking with explicit scheduler and symbolic threads
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- An automatic method for the dynamic construction of abstractions of states of a formal model
- A novel analysis space for pointer analysis and its application for bug finding
- Optimistic synchronization-based state-space reduction
- Stateless model checking for TSO and PSO
- scientific article; zbMATH DE number 5850137 (Why is no real title available?)
- scientific article; zbMATH DE number 1956607 (Why is no real title available?)
- Tools and Algorithms for the Construction and Analysis of Systems
- Symbolic predictive analysis for concurrent programs
- Distributed verification of multi-threaded C++ programs
- scientific article; zbMATH DE number 1863159 (Why is no real title available?)
- Complexity reduction in MPC for stochastic max-plus-linear discrete event systems by variability expansion
- scientific article; zbMATH DE number 2080308 (Why is no real title available?)
- Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction
- Combining model checking and testing
- Rule-based static analysis of network protocol implementations
- Global reproducibility through local control for distributed active objects
- Computer Aided Verification
- APS-1
- Zing
- Quasar
- POOC
- Symstra
- StEAM
- SyncGen
- TVOC
- BLAST
- VLISP
- PROD
- SLAM
- SPIN
- Helena
- ISP
- General Purpose Hash Function Library
- Bogor
- ADL
- DART
- Korat
- PathCrawler
- Rostra
- visualSTATE
- Bandera
- ACL2s
- Java PathFinder
- KRATOS
- SystemC
- CESAR
- Atomizer
- Bebop
- APS
- Eraser
- STMBench7
- ConTest
- Lee-TM
- cminor
- dSPIN
- Checkfence
- JPAX
- CCured
- vUML
- SingleTrack
- Pinapa
- Specomp
- WormBench
- MOPS
- TVLA
- JPF-SE
- Specware
- DPF
- GDB
- MODIST
- ALPBench
- LusSy
- CodeSurfer
- monabs
- Angelic Verification
- Syco
- Kit
- Guava
This page was built for software: veriSoft