33 citations · 56 across the 10 of their papers we have counts for
7 papers · 1 filter
Data-driven Verification of Procedural Programs with Integer Arrays
Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl
We address the problem of verifying automatically procedural programs manipulating parametric-size arrays of integers, encoded as a constrained Horn clauses solving problem. We pro…
Automated Synthesis of Asynchronizations
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea +1
Asynchronous programming is widely adopted for building responsive and efficient software, and modern languages such as C# provide async/await primitives to simplify the use of asy…
Checking Robustness Between Weak Transactional Consistency Models
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
Concurrent accesses to databases are typically encapsulated in transactions in order to enable isolation from other concurrent computations and resilience to failures. Modern datab…
On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony
Ahmed Bouajjani, Constantin Enea, Kailiang Ji +1
We address the problem of verifying message passing programs, defined as a set of parallel processes communicating through unbounded FIFO buffers. We introduce a bounded analysis t…
Checking Linearizability of Concurrent Priority Queues
Ahmed Bouajjani, Constantin Enea, Chao Wang
Efficient implementations of concurrent objects such as atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchroniza…
Proving linearizability using forward simulations
Ahmed Bouajjani, Michael Emmi, Constantin Enea +1
Linearizability is the standard correctness criterion concurrent data structures such as stacks and queues. It allows to establish observational refinement between a concurrent imp…