29 citations · 49 across the 9 of their papers we have counts for
5 papers · 1 filter
NP Decision Procedure for Monomial and Linear Integer Constraints
Rodrigo Raya, Jad Hamza, Viktor Kunčak
Motivated by satisfiability of constraints with function symbols, we consider numerical inequalities on non-negative integers. The constraints we consider are a conjunction of a li…
System FR as Foundations for Stainless
Jad Hamza, Nicolas Voirol, Viktor Kunčak
We present the design, implementation, and foundation of a verifier for higher-order functional programs with generics and recursive data types. Our system supports proving safety…
On Verifying Causal Consistency
Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui +1
Causal consistency is one of the most adopted consistency criteria for distributed implementations of data structures. It ensures that operations are executed at all sites accordin…
On Reducing Linearizability to State Reachability
Ahmed Bouajjani, Michael Emmi, Constantin Enea +1
Efficient implementations of atomic objects such as concurrent stacks and queues are especially susceptible to programming errors, and necessitate automatic verification. Unfortuna…
On the complexity of Linearizability
Jad Hamza
It was shown in Alur et al. [1] that the problem of verifying finite concurrent systems through Linearizability is in EXPSPACE. However, there was still a complexity gap between th…