29 citations · 49 across the 9 of their papers we have counts for
12 papers
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…
Coming to Terms with Your Choices: An Existential Take on Dependent Types
Georg Stefan Schmid, Olivier Blanvillain, Jad Hamza +1
Type-level programming is an increasingly popular way to obtain additional type safety. Unfortunately, it remains a second-class citizen in the majority of industrially-used progra…
Can 100 Machines Agree?
Rachid Guerraoui, Jad Hamza, Dragos-Adrian Seredinschi +1
Agreement protocols have been typically deployed at small scale, e.g., using three to five machines. This is because these protocols seem to suffer from a sharp performance decay.…
LL(1) Parsing with Derivatives and Zippers
Romain Edelmann, Jad Hamza, Viktor Kunčak
In this paper, we present an efficient, functional, and formally verified parsing algorithm for LL(1) context-free expressions based on the concept of derivatives of formal languag…
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…
Monotonic Prefix Consistency in Distributed Systems
Alain Girault, Gregor Gössler, Rachid Guerraoui +2
We study the issue of data consistency in distributed systems. Specifically, we consider a distributed system that replicates its data at multiple sites, which is prone to partitio…