 |
|
gilad arnold |
|
גלעד ארנולד
|
|
hi!
I'm a graduate student of
Computer Science at
UC Berkeley.
My work focuses on programming models and analysis of programs manipulating
large irregular data. I deal with language design, formal verification,
analysis and synthesis of programs. I'm specifically interested in design of
clean languages for specific problem domains, and coupling them with powerful
tools for verification and generation of code. I currently work on sparse
matrix codes. I'm being advised by
Prof. Ras Bodík and part of
The Parallel Computing
Laboratory.
publications
-
Specifying and Verifying Sparse Matrix Codes
Gilad Arnold,
Johannes Hölzl,
Ali Sinan Köksal ,
Rastislav Bodík,
and
Mooly Sagiv
ICFP '10:
The 15th ACM SIGPLAN International Conference on Functional Programming
[ps]
[pdf]
[slides-pdf]
© ACM
-
Sketching Stencils
Armando Solar-Lezama,
Gilad Arnold,
Liviu Tancau,
Rastislav Bodík,
Vijay
Saraswat,
and
Sanjit Seshia
PLDI '07:
ACM SIGPLAN 2007 Conference on Programming Language Design and
Implementation
[ps]
[pdf]
© ACM
-
Specialized 3-Valued Logic Shape Analysis using
Structure-Based Refinement and Loose Embedding
Gilad Arnold
SAS '06:
The 13th International Static Analysis Symposium
[ps]
[pdf]
[slides-ps]
© Springer-Verlag
-
Combining Shape Analyses by Intersecting
Abstractions
Gilad Arnold,
Roman Manevich,
Mooly Sagiv, and
Ran Shaham
VMCAI '06:
The 7th International Conference on Verification, Model Checking
and Abstract Interpretation
[ps]
[pdf]
[slides-ps]
© Springer-Verlag
-
Lightweight Specialized 3-Valued Logic Shape
Analyzer
Gilad Arnold
Technical report EECS-2006-59, EECS Department, UC Berkeley, 2006
[pdf]
-
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, Tel-Aviv University, 2004
[ps]
[pdf]
-
Combining Heap Analyses by Intersecting
Abstractions
Gilad Arnold
Master's thesis, Tel-Aviv University
[ps]
[pdf]
[slides-ps]
projects
teaching
coursework
-
Symbolic Proof Generation for Resizing Sketches
CS294-9: Interactive Computer Theorem Proving (Fall '06)
(with Liviu Tancau)
[ps]
[pdf]
[slides]
-
Extending the Applicability of Sketching
CS294-2: Software Synthesis + EE219C: Computer-Aided Verification (Spring '06)
(with Armando Solar-Lezama
and Liviu Tancau)
[ps]
[pdf]
[slides]
-
Improving Scalability of 3-Valued Logic Shape Analysis by
Loosening Embedding
CS263: Design and Analysis of Programming Languages (Fall '05)
[ps]
[pdf]
[slides]
-
Topology-Based Approach for Lightweight 3-Valued Logic Shape
Analysis
CS264: Program Analysis (Spring '05)
[ps]
[pdf]
[slides]
-
pobj: A Lightweight Persistent Objects Library and Its Applications to
Persistency in Titanium/Java
CS262a: Advanced Topics in Computer Systems (Fall '04)
(with Amir Kamil)
[pdf]
[poster]
personal
Before coming to Berkeley, I completed my masters at Tel-Aviv University under the supervision
of Prof. Mooly Sagiv. It was
then that I developed interest in heap analysis and abstract interpretation.
For a few years I was a full-time software engineer at Terayon Communication Systems (previously
ComBox, currently Motorola) where I wrote networking and real-time code for
a variety of embedded router platforms.
While working on IP routing in Linux, I became involved with open-source
routing software and contributed to the Quagga project, an actively maintained fork
of the popular GNU Zebra.
In the course of previous occupations I was also a sysadmin, a combat sniper,
a keyboardist, and a telephone technician.
These days I try to juggle between research and several other things, like
running, swimming, and music. I also run the Berkeley List of Israeli Students
and Scholars (aka BLISS).
I grew up in Petah
Tikva, a gray and generally uninspiring city not far from Tel-Aviv. Still, it
is my hometown.
stuff