Symbolic predictive analysis for concurrent programs

DOI10.1007/s00165-011-0179-2zbMath1242.68187OpenAlexW2033651910MaRDI QIDQ432146

Rhishikesh Limaye, Sudipta Kundu, Aarti Gupta, Chao Wang, Malay K. Ganai

Publication date: 3 July 2012

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-011-0179-2

zbMATH Keywords

SATSMTconcurrent trace programcontext boundinghappens-beforepredictive analysis

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Model Checking Concurrent Programs, Thread-modular analysis of release-acquire concurrency, Symbolic predictive analysis for concurrent programs, Dynamic symbolic verification of MPI programs

Uses Software

• veriSoft
• Java PathFinder
• Eraser
• Atomizer
• Velodrome
• CBMC
• SingleTrack
• Checkfence
• Java Grande
• CHESS
• AVIO
• CIL

Cites Work

• Unnamed Item
• Unnamed Item
• Symbolic predictive analysis for concurrent programs
• Atomizer: A dynamic atomicity checker for multithreaded programs
• Model checking JAVA programs using JAVA PathFinder
• Back to the future
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
• Monitoring Atomicity in Concurrent Programs
• Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
• Trace-Based Symbolic Analysis for Atomicity Violations
• SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs
• The Complexity of Predicting Atomicity Violations
• Meta-analysis for Atomicity Violations under Nested Locking
• Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
• Time, clocks, and the ordering of events in a distributed system
• Platform independent dynamic Java virtual machine analysis: the Java Grande Forum benchmark suite
• Dynamic partial-order reduction for model checking software
• Tools and Algorithms for the Construction and Analysis of Systems
• Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
• Parametric and Sliced Causality
• Peephole Partial Order Reduction
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Causal Atomicity