I am a Postdoc at the Department of Computer Sciences at the University of Texas at Austin (UT), a member of the Intelligent Systems Group of Prof. Keshav Pingali.

Before that I was a Postdoc researcher at the Computer Science Department of the University of California Los Angeles (UCLA) on the team of Prof. Rupak Majumdar.

Before that I was a Ph.D. student of Computer Science at Tel-Aviv University, advised by Prof. Shmuel (Mooly) Sagiv.

I am generally interested in formal verification of computer programs, especially by Abstract interpretation. My main background is in Shape Analysis, which is the problem of inferring structural properties of dynamically allocated data structures.

Publications

PhD thesis: Partially Disjunctive Shape Analysis
[bib] [abstract] [pdf] [ppt] [Hebrew part]

Master's thesis: Data Structures and Algorithms for Efficient Shape Analysis
[bib] [abstract] [pdf] [ps] [ppt] [cover pages]

Abstract Transformers for Thread Correlation Analysis
Michal Segalov, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, and Mooly Sagiv.
To appear in APLAS'09: The Seventh Asian Symposium on Programming Languages and Systems, Seoul, Korea, December 2009.

Thread Quantification for Concurrent Shape Analysis
Josh Berdine, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, and Mooly Sagiv.
Appeared in CAV'08: 20th International Conference on Computer Aided Verification, Princeton, USA, July 2008. © Springer-Verlag [abstract] [pdf] [Tech. report] [ppt]

Heap Decomposition for Concurrent Shape Analysis
Roman Manevich, Tal Lev-Ami, Ganesan Ramalingam, Mooly Sagiv, and Josh Berdine.
Appeared in SAS'08: 15th International Static Analysis Symposium, Valencia, Spain, July 2008 © Springer-Verlag [abstract] [pdf] [Tech. report] [ppt]

Shape Analysis by Graph Decomposition
Roman Manevich, Josh Berdine, Byron Cook, Ganesan Ramalingam, and Mooly Sagiv.
Appeared in TACAS'07: 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Braga, Portugal, March 2007
© Springer-Verlag [bib] [abstract] [pdf] [full version] [ppt]

Abstract Counterexample-based Refinement for Powerset Domains
Roman Manevich, John Field, Thomas A. Henzinger, Ganesan Ramalingam, and Mooly Sagiv.
Appeared in Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm © Springer-Verlag [bib] [abstract] [pdf]

Combining Shape Analyses by Intersecting Abstractions
Gilad Arnold, Roman Manevich, Mooly Sagiv, and Ran Shaham.
VMCAI '06: 7th Conference on Verification, Model Checking and Abstract Interpretation, Charleston, South Carolina, U.S.A., January 2006
© Springer-Verlag [bib] [abstract] [ps] [pdf] [Gilad's slides]

Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists
Roman Manevich, Eran Yahav, Ganesan Ramalingam, and Mooly Sagiv.
VMCAI '05: 6th Conference on Verification, Model Checking and Abstract Interpretation, Paris, January 2005 © Springer-Verlag [bib] [abstract] [ps] [pdf] [ppt]

PSE: Explaining Program Failures via Postmortem Static Analysis
Roman Manevich, Manu Sridharan, Stephen Adams, Manuvir Das, and Zhe Yang.
FSE '04: 12th International Symposium on the Foundations of Software Engineering, Newport Beach, November 2004
© ACM [bib] [abstract] [pdf] (ACM link) [Manu's slides]

Partially Disjunctive Heap Abstraction
Roman Manevich, Mooly Sagiv, Ganesan Ramalingam, and John Field.
SAS '04: 11th International Static Analysis Symposium, Verona, August 2004
© Springer-Verlag [bib] [abstract] [pdf] [ps] [ppt]

TVLA: A System for Generating Abstract Interpreters
Tal Lev-Ami, Roman Manevich, and Mooly Sagiv.
IFIP '04: The 18th World Computer Congress, Toulouse, France, August 2004
Invited paper, presented at the topical day on abstract interpretation
© Springer-Verlag [bib] [abstract] [pdf] [ppt]

Compactly Representing First-Order Structures for Static Analysis
Roman Manevich, Ganesan Ramalingam, John Field, Deepak Goyal, and Mooly Sagiv.
SAS '02: The 9th International Static Analysis Symposium, Madrid, September 2002
© Springer-Verlag [bib] [abstract] [pdf] [ps] [ppt]

Technical Reports and Non-refereed Publications

Heap Decomposition for Concurrent Shape Analysis
Roman Manevich, Tal Lev-Ami, Ganesan Ramalingam, Mooly Sagiv, and Josh Berdine.
Technical Report TR-2007-11-85453 [bib] [abstract] [pdf] [Dagstuhl talk]

Automatic Verification of Strongly Dynamic Software Systems
N. Dor, J. Field, D. Gopan, T. Lev-Ami, A. Loginov, R. Manevich, G. Ramalingam, T. Reps, N. Rinetzky, M. Sagiv, R. Wilhelm, E. Yahav, and G. Yorsh.
Proc. IFIP Working Conference on Verified Software: Theories, Tools, Experiments, Zurich, Switzerland, Oct. 10-13, 2005 [abstract] [pdf]

Lightweight Analysis of Acyclic Unshared Lists
Roman Manevich, Shuvendu K. Lahiri, and Mooly Sagiv.
Technical Report TR-2005-12-1297820 [bib] [abstract] [pdf] [ps]

Intersecting Heap Abstractions with Applications to Compile-time Memory Management
Gilad Arnold, Roman Manevich, Mooly Sagiv, and Ran Shaham.
Technical Report TR-2005-04-135520 [bib] [abstract] [pdf] [ps]

Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists
Roman Manevich, E. Yahav, Ganesan Ramalingam, and Mooly Sagiv.
Technical report TR-2005-01-191212 [pdf] [ps]

Software

3-Valued Logic Analyzer is a powerful framework for Shape Analysis.

J2TVLA is a Soot-based toolkit for translating Java programs to TVLA inputs.
I no longer actively maintain J2TVLA, but if you are interested in using it, contact me for further details.

Teaching Assistance

Winter 2007-2008 Compilation Course 0368.3133
Winter 2006-2007 Compilation Course 0368.3133
Instructor: Prof. Shmuel (Mooly) Sagiv

Music Links

Tom Waits
Funk'n'Stein
Macy Gray
Matti Caspi (An Israeli artist)
Gipsy Kings (click on Artist's web site for sound samples)
Cape Verde - Cesaria Evora - Folk singer
Latin radio Batanga



  Classical Guitar

The Classical Guitar Home Page
The Classical Guitar midi archives
Guitar Seek
Guitar Notes
Guitar Tabs
Manuel Raimundo guitars
Los Angeles Classical Guitars