 |
|
gilad arnold |
|
גלעד ארנולד
|
|
welcome!
I'm a graduate student of
Computer Science at
UC Berkeley.
My work focuses on synthesis of programs that manipulate unbounded data using
abstraction and symbolic proofs. I currently work on verification and
synthesis of sparse matrix code. I'm being advised by
Prof. Ras Bodik and I am part
of the
The Parallel Computing
Laboratory.
My interests also include static analysis and verficiation,
software engineering, and algorithm design.
publications
-
Sketching Stencils
Armando Solar-Lezama,
Gilad Arnold,
Liviu Tancau,
Rastislav Bodik,
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:
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:
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 also was a software tester and
sysadmin, a sniper and heavy mortar operator, a keyboardist, and a telephone
technician.
These days I try to juggle between research and several other things, like
fighting for affordable daycare for
student families, long distance running, basketball, and music.
I grew up in Petah
Tikva, a gray and generally uninspiring city not far from Tel-Aviv. Still, it
is my hometown.
stuff