Automatic analysis of DMA races using model checking and \(k\)-induction

DOI10.1007/s10703-011-0124-2zbMath1233.68124OpenAlexW2120162396MaRDI QIDQ763238

Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer

Publication date: 9 March 2012

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-011-0124-2

zbMATH Keywords

model checkingDMA\(k\)-inductionmulticore programmingCell BE

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Latticed \(k\)-induction with an application to probabilistic programs ⋮ Backward symbolic execution with loop folding ⋮ k-Inductive Barrier Certificates for Stochastic Systems ⋮ Strengthening Induction-Based Race Checking with Lightweight Static Analysis ⋮ SCRATCH

Uses Software

• MiniSat
• BLAST
• Cellss
• Eraser
• CBMC
• RacerX
• SatAbs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The existence of refinement mappings
• Reducing concurrent analysis under a context bound to sequential analysis
• Strengthening Induction-Based Race Checking with Lightweight Static Analysis
• On folk theorems
• Dynamic partial-order reduction for model checking software
• Tools and Algorithms for the Construction and Analysis of Systems
• Making prophecies with decision predicates
• Delay-bounded scheduling
• Tools and Algorithms for the Construction and Analysis of Systems