veriSoft
From MaRDI portal
Software:14223
swMATH1489MaRDI QIDQ14223FDOQ14223
Author name not available (Why is that?)
Cited In (74)
- Syntax-directed model checking of sequential programs
- Global Reproducibility Through Local Control for Distributed Active Objects
- Title not available (Why is that?)
- Title not available (Why is that?)
- Effective Program Verification for Relaxed Memory Models
- Delay-bounded scheduling without delay!
- Stateless model checking under a reads-value-from equivalence
- A formally verified compiler back-end
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions
- 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
- Model Checking Software
- Tools and Algorithms for the Construction and Analysis of Systems
- Proving the correctness of client/server software
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- An automatic method for the dynamic construction of abstractions of states of a formal model
- Automation of Quantitative Information-Flow Analysis
- A novel analysis space for pointer analysis and its application for bug finding
- Title not available (Why is that?)
- Title not available (Why is that?)
- Stateless model checking for TSO and PSO
- Optimistic synchronization-based state-space reduction
- Tools and Algorithms for the Construction and Analysis of Systems
- Distributed verification of multi-threaded C++ programs
- Symbolic predictive analysis for concurrent programs
- Title not available (Why is that?)
- Model Checking Concurrent Programs
- Complexity reduction in MPC for stochastic max-plus-linear discrete event systems by variability expansion
- Computer Aided Verification
- Rule-based static analysis of network protocol implementations
- Title not available (Why is that?)
- Multithreaded testing of program interfaces
- Tools and Algorithms for the Construction and Analysis of Systems
- Title not available (Why is that?)
- Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures
- Certifying low-level programs with hardware interrupts and preemptive threads
- Model Checking Software
- Partial order reduction for rewriting semantics of programming languages
- Wireless protocol validation under uncertainty
- Model Checking Database Applications
- Software Model Checking: Searching for Computations in the Abstract or the Concrete
- Quasi-optimal partial order reduction
- A compositional behavioral modeling framework for embedded system design and conformance checking
- Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings
- Operating system verification---an overview
- Full simulation coverage for SystemC transaction-level models of systems-on-a-chip
- Extensible transactional memory testbed
- On the correctness of upper layers of automotive systems
- Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs
- Mechanized semantics for the clight subset of the C language
- Model Checking Software
- Proving fairness and implementation correctness of a microkernel scheduler
- Computer Aided Verification
- Static analysis for state-space reductions preserving temporal logics
- Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs
- An overview of the runtime verification tool Java PathExplorer
- Validation of Stochastic Systems
- Translating Java for multiple model checkers: The Bandera back-end
- Verifying time partitioning in the DEOS scheduling kernel
- Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
- State Space Reduction of Rewrite Theories Using Invisible Transitions
- Software model checking with explicit scheduler and symbolic threads
- Title not available (Why is that?)
- Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction
- Model Checking Software
- A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems
- Validation of Stochastic Systems
- Combining Model Checking and Testing
- Boosting Lazy Abstraction for SystemC with Partial Order Reduction
- Dynamic Path Reduction for Software Model Checking
This page was built for software: veriSoft