Search

• < Previous
• 1
• Next >

---

A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes

Ahmed Bouajjani ; Cezara Dragoi ; Constantin Enea ; Yan Jurski ; Mihaela Sighireanu.

We propose a framework for reasoning about unbounded dynamic networks of infinite-state processes. We propose Constrained Petri Nets (CPN) as generic models for these networks. They can be seen as Petri nets where tokens (representing occurrences of processes) are colored by values over some&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;]

---