Putting static analysis to work for verification: A case study. - Tal Lev-Ami; Thomas W. Reps; Shmuel Sagiv; Reinhard Wilhelm (ISSTA, 2000)

TVLA: A System for Implementing Static Analyses. - Tal Lev-Ami; Shmuel Sagiv (SAS, 2000)

Reactive and Real-Time Systems Course: How to Get the Most Out of it. - Tal Lev-Ami; Shmuel S. Tyszberowicz (Real Time Syst., 2003)

TVLA: A system for generating abstract interpreters. - Tal Lev-Ami; Roman Manevich; Shmuel Sagiv (IFIP Congress Topical Sessions, 2004)

Automatic Verification of Strongly Dynamic Software Systems. - Nurit Dor; John Field; Denis Gopan; Tal Lev-Ami; Alexey Loginov; Roman Manevich; G. Ramalingam; Thomas W. Reps; Noam Rinetzky; Mooly Sagiv; Reinhard Wilhelm; Eran Yahav; et al. (VSTTE, 2005)

Abstraction for Shape Analysis with Fast and Precise Transformers. - Tal Lev-Ami; Neil Immerman; Shmuel Sagiv (CAV, 2006)

Labelled Clauses. - Tal Lev-Ami; Christoph Weidenbach; Thomas W. Reps; Mooly Sagiv (CADE, 2007)

Revamping TVLA: Making Parametric Shape Analysis Competitive. - Igor Bogudlov; Tal Lev-Ami; Thomas W. Reps; Mooly Sagiv (CAV, 2007)

Constructing Specialized Shape Analyses for Uniform Change. - Tal Lev-Ami; Mooly Sagiv; Neil Immerman; Thomas W. Reps (VMCAI, 2007)

Thread Quantification for Concurrent Shape Analysis. - Josh Berdine; Tal Lev-Ami; Roman Manevich; G. Ramalingam; Shmuel Sagiv (CAV, 2008)

Proving Conditional Termination. - Byron Cook; Sumit Gulwani; Tal Lev-Ami; Andrey Rybalchenko; Mooly Sagiv (CAV, 2008)

Customization change impact analysis for erp professionals via program slicing. - Nurit Dor; Tal Lev-Ami; Shay Litvak; Mooly Sagiv; Dror Weiss (ISSTA, 2008)

Heap Decomposition for Concurrent Shape Analysis. - Roman Manevich; Tal Lev-Ami; Mooly Sagiv; Ganesan Ramalingam; Josh Berdine (SAS, 2008)

Abstract Transformers for Thread Correlation Analysis. - Michal Segalov; Tal Lev-Ami; Roman Manevich; Ganesan Ramalingam; Mooly Sagiv (APLAS, 2009)

A combination framework for tracking partition sizes. - Sumit Gulwani; Tal Lev-Ami; Mooly Sagiv (POPL, 2009)

Simulating reachability using first-order logic with applications to verification of linked data structures - Tal Lev-Ami; Neil Immerman; Thomas W. Reps; Mooly Sagiv; Siddharth Srivastava 001; Greta Yorsh (Log. Methods Comput. Sci., 2009)

Automatic maintenance of transitive properties with applications to shape analysis - Tal Lev-Ami (2009)

The JPEG XL Image Coding System: History, Features, Coding Tools, Design Rationale, and Future. - Jon Sneyers; Jyrki Alakuijala; Luca Versari; Zoltan Szabadka; Sami Boukortt; Amnon Cohen-Tidhar; Moritz Firsching; Evgenii Kliuchnikov; Tal Lev-Ami; Eric Portis; Thomas Richter 005; Osamu Watanabe (CoRR, 2025)