veriSoft

swMATH1489MaRDI QIDQ14223FDOQ14223

Author name not available (Why is that?)

Described by source

• Compositional analysis of C/C++ programs with veriSoft

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