Search

• < Previous
• 1
• Next >

---

Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads

Mohamed Faouzi Atig ; Ahmed Bouajjani ; Shaz Qadeer.

Context-bounded analysis has been shown to be both efficient and effective at finding bugs in concurrent programs. According to its original definition, context-bounded analysis explores all behaviors of a concurrent program up to some fixed number of context switches between threads. This&nbsp;[&hellip;]

---

Model-Checking of Ordered Multi-Pushdown Automata

Mohamed Faouzi Atig.

We address the verification problem of ordered multi-pushdown automata: A multi-stack extension of pushdown automata that comes with a constraint on stack transitions such that a pop can only be performed on the first non-empty stack. First, we show that the emptiness problem for ordered&nbsp;[&hellip;]

---

Mending Fences with Self-Invalidation and Self-Downgrade

Parosh Aziz Abdulla ; Mohamed Faouzi Atig ; Stefanos Kaxiras ; Carl Leonardsson ; Alberto Ros ; Yunyun Zhu.

Cache coherence protocols based on self-invalidation and self-downgrade have recently seen increased popularity due to their simplicity, potential performance efficiency, and low energy consumption. However, such protocols result in memory instruction reordering, thus causing extra program behaviors&nbsp;[&hellip;]

---

A Load-Buffer Semantics for Total Store Ordering

Parosh Aziz Abdulla ; Mohamed Faouzi Atig ; Ahmed Bouajjani ; Tuan Phong Ngo.

We address the problem of verifying safety properties of concurrent programs running over the Total Store Order (TSO) memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is&nbsp;[&hellip;]

---