Context-bounded model checking of concurrent software
From MaRDI portal
Recommendations
- Computer Aided Verification
- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
- Interprocedural Analysis of Concurrent Programs Under a Context Bound
- Reducing concurrent analysis under a context bound to sequential analysis
- Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads
Cited in
(86)- Reducing concurrent analysis under a context bound to sequential analysis
- Realizability of concurrent recursive programs
- Compact and efficiently verifiable models for concurrent systems
- Static analysis of embedded real-time concurrent software with dynamic priorities
- Model checking concurrency and causality
- Incremental bounded model checking for embedded software
- An automata-theoretic approach to the verification of distributed algorithms
- Verifying parallel programs with dynamic communication structures
- Model checking of concurrent software systems via heuristic-guided SAT solving
- Reachability of scope-bounded multistack pushdown systems
- Analysis of correct synchronization of operating system components
- Leafy automata for higher-order concurrency
- The decidability of verification under PS 2.0
- On exteriority notions in book embeddings and treewidth
- Verification of SpecC using predicate abstraction
- The complexity of model checking multi-stack systems
- Verification of Boolean programs with unbounded thread creation
- Recent advances on reachability problems for valence systems (invited talk)
- BDD vs. constraint-based model checking: An experiment evaluation for asynchronous concurrent systems
- CCA-secure keyed-fully homomorphic encryption
- Verification of parameterized communicating automata via split-width
- Context-free ambiguity detection using multi-stack pushdown automata
- On symbolic verification of weakly extended PAD
- Model checking concurrent programs with nondeterminism and randomization
- Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
- Faster algorithms for weighted recursive state machines
- Static analysis of run-time errors in embedded critical parallel C programs
- Reachability of multistack pushdown systems with scope-bounded matching relations
- Reasoning about threads with bounded lock chains
- The complexity of reversal-bounded model-checking
- SAT-Based Model Checking
- Model checking concurrent programs
- Combining model checking and testing
- On Distributed Monitoring and Synthesis
- Parameterized Verification of Communicating Automata under Context Bounds
- Automated synthesis of distributed controllers
- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
- scientific article; zbMATH DE number 5353387 (Why is no real title available?)
- Games on Multi-stack Pushdown Systems
- Realizability of Concurrent Recursive Programs
- Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads
- Verifying Parallel Programs with Dynamic Communication Structures
- Games on Higher Order Multi-stack Pushdown Systems
- Reducing behavioural to structural properties of programs with procedures
- Symbolic predictive analysis for concurrent programs
- Verification of STM on relaxed memory models
- Bounded underapproximations
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
- Emptiness of ordered multi-pushdown automata is 2ETIME-complete
- Temporal logics for concurrent recursive programs: satisfiability and model checking
- Budget-bounded model-checking pushdown systems
- Bounded context switching for valence systems
- Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous
- Data multi-pushdown automata
- On the Complexity of Bounded Context Switching.
- Verification of asynchronous programs with nested locks
- On the path-width of integer linear programming
- Context-bounded analysis of TSO systems
- Bounded communication reachability analysis of process rewrite systems with ordered parallelism
- Zing: Exploiting program structure for model checking concurrent software
- Model checking with bounded context switching
- Interprocedural Analysis of Concurrent Programs Under a Context Bound
- Context-Bounded Analysis of Concurrent Queue Systems
- Program Analysis Using Weighted Pushdown Systems
- Computer Aided Verification
- Reachability analysis of pushdown systems with an upper stack
- Model-Checking HyperLTL for Pushdown Systems
- Decidable models of integer-manipulating programs with recursive parallelism
- Fine-grained complexity of safety verification
- A pragmatic approach to stateful partial order reduction
- Reconciling preemption bounding with DPOR
- Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models
- Forwards- and backwards-reachability for cooperating multi-pushdown systems
- Round- and context-bounded control of dynamic pushdown systems
- Reasoning about reversal-bounded counter machines
- HyperMonitor: a Python prototype for hyper predictive runtime verification
- Backwards-reachability for cooperating multi-pushdown systems
- On the complexity of multi-pushdown games
- The complexity of bounded context switching with dynamic thread creation
- Phase-bounded broadcast networks over topologies of communication
- Model-checking parametric lock-sharing systems against regular constraints
- LTL model checking of concurrent self-modifying code
- Unboundedness problems for formal languages (invited talk)
- Delay-bounded scheduling without delay!
- Compositional verification of sequential programs with procedures
- Verification of well-formed communicating recursive state machines
This page was built for publication: Context-bounded model checking of concurrent software
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5703798)
