Synthesis for regular specifications over unbounded domains. - Jad Hamza; Barbara Jobstmann; Viktor Kuncak (FMCAD, 2010)

Verifying Concurrent Programs against Sequential Specifications. - Ahmed Bouajjani; Michael Emmi; Constantin Enea; Jad Hamza (ESOP, 2013)

Verifying eventual consistency of optimistic replication systems. - Ahmed Bouajjani; Constantin Enea; Jad Hamza (POPL, 2014)

Linearizability is EXPSPACE-complete. - Jad Hamza (CoRR, 2014)

Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk). - Ahmed Bouajjani; Michael Emmi; Constantin Enea; Jad Hamza (FSTTCS, 2015)

Monitoring refinement via symbolic reasoning. - Michael Emmi; Constantin Enea; Jad Hamza (PLDI, 2015)

Tractable Refinement Checking for Concurrent Objects. - Ahmed Bouajjani; Michael Emmi; Constantin Enea; Jad Hamza (POPL, 2015)

Optimal Test Sets for Context-Free Languages. - Mikaël Mayer; Jad Hamza (CoRR, 2016)

Proactive Synthesis of Recursive Tree-to-String Functions from Examples. - Mikaël Mayer; Jad Hamza; Viktor Kuncak (ECOOP, 2017)

On verifying causal consistency. - Ahmed Bouajjani; Constantin Enea; Rachid Guerraoui; Jad Hamza (POPL, 2017)

Polynomial-Time Proactive Synthesis of Tree-to-String Functions from Examples. - Mikaël Mayer; Jad Hamza; Viktor Kuncak (CoRR, 2017)

Why You Can't Beat Blockchains: Consistency and High Availability in Distributed Systems. - Alain Girault; Gregor Gößler; Rachid Guerraoui; Jad Hamza; Dragos-Adrian Seredinschi (CoRR, 2017)

Proactive Synthesis of Recursive Tree-to-String Functions from Examples (Artifact). - Mikaël Mayer; Jad Hamza; Viktor Kuncak (Dagstuhl Artifacts Ser., 2017)

Monotonic Prefix Consistency in Distributed Systems. - Alain Girault; Gregor Gößler; Rachid Guerraoui; Jad Hamza; Dragos-Adrian Seredinschi (FORTE, 2018)

On reducing linearizability to state reachability. - Ahmed Bouajjani; Michael Emmi; Constantin Enea; Jad Hamza (Inf. Comput., 2018)

Minimal Synthesis of String to String Functions from Examples. - Jad Hamza; Viktor Kuncak (VMCAI, 2019)

On the complexity of linearizability. - Jad Hamza (Computing, 2019)

System FR as Foundations for Stainless. - Jad Hamza; Nicolas Voirol; Viktor Kuncak (CoRR, 2019)

Can 100 Machines Agree? - Rachid Guerraoui; Jad Hamza; Dragos-Adrian Seredinschi; Marko Vukolic (CoRR, 2019)

LL(1) Parsing with Derivatives and Zippers. - Romain Edelmann; Jad Hamza; Viktor Kuncak (CoRR, 2019)

System FR: formalized foundations for the stainless verifier. - Jad Hamza; Nicolas Voirol; Viktor Kuncak (Proc. ACM Program. Lang., 2019)

Zippy LL(1) parsing with derivatives. - Romain Edelmann; Jad Hamza; Viktor Kuncak (PLDI, 2020)

Coming to Terms with Your Choices: An Existential Take on Dependent Types. - Georg Stefan Schmid; Olivier Blanvillain; Jad Hamza; Viktor Kuncak (CoRR, 2020)

Stainless Verification System Tutorial. - Viktor Kuncak; Jad Hamza (FMCAD, 2021)

From Verified Scala to STIX File System Embedded Code Using Stainless. - Jad Hamza; Simon Felix; Viktor Kuncak; Ivo Nussbaumer; Filip Schramka (NFM, 2022)

NP Decision Procedure for Monomial and Linear Integer Constraints. - Rodrigo Raya; Jad Hamza; Viktor Kuncak (CoRR, 2022)

On the Complexity of Convex and Reverse Convex Prequadratic Constraints. - Rodrigo Raya; Jad Hamza; Viktor Kuncak (LPAR, 2023)