Dynamic partial-order reduction for model checking software
From MaRDI portal
Publication:5276139
DOI10.1145/1040305.1040315zbMath1369.68135MaRDI QIDQ5276139
Cormac Flanagan, Patrice Godefroid
Publication date: 14 July 2017
Published in: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://escholarship.org/uc/item/47c9f29c
68N19: Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Unnamed Item, Global Reproducibility Through Local Control for Distributed Active Objects, Local Data Race Freedom with Non-multi-copy Atomicity, Analysis and Transformation of Constrained Horn Clauses for Program Verification, Prefix-based tracing in message-passing concurrency, A pragmatic approach to stateful partial order reduction, Quantifiability: a concurrent correctness condition modeled in vector space, Unfolding-based dynamic partial order reduction of asynchronous distributed programs, A geometric view of partial order reduction, Symbolic predictive analysis for concurrent programs, Context-aware counter abstraction, Bisimulation conversion and verification procedure for goal-based control systems, Composing model programs for analysis, Automatic analysis of DMA races using model checking and \(k\)-induction, Stateless model checking under a reads-value-from equivalence, Symmetry and partial order reduction techniques in model checking Rebeca, Full simulation coverage for SystemC transaction-level models of systems-on-a-chip, Stateless model checking for TSO and PSO, Actor-based model checking for software-defined networks, SDN-actors: modeling and verification of SDN programs, Approximate partial order reduction, Operational semantics with semicommutations, Quasi-optimal partial order reduction, Verifying the correctness of distributed systems via mergeable parallelism, Computing race variants in message-passing concurrent programming with selective receives, POR for security protocol equivalences. Beyond action-determinism, Compositional verification of asynchronous concurrent systems using CADP, Verification of SpecC using predicate abstraction, Multithreaded testing of program interfaces, Partial Order Reduction for Rewriting Semantics of Programming Languages, Independence Abstractions and Models of Concurrency, Dynamic Reductions for Model Checking Concurrent Software, Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models, Model Checking Concurrent Programs, Combining Model Checking and Testing, Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems, Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings, Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions, Dynamic Partial Order Reduction Using Probe Sets, Exploring the Scope for Partial Order Reduction
