 |
|
gilad arnold |
|
גלעד ארנולד
|
|
welcome!
I'm a fourth-year graduate student of
Computer Science at
UC Berkeley.
I am part of the SKETCH project
and work on synthesis of unbounded computations using abstraction and symbolic
proofs. My advisor is
Prof. Ras Bodik.
My interests also include static analysis
and verficiation (in particular
shape analysis using 3-valued logic), 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 operated a sniper rifle, a heavy mortar, and
a few similar instruments. I've since shifted towards more peaceful
activities.
I love music. I played piano
and elecronic
keyboards for many years, and I'm an obsessive listener to various
genres including jazz, R&B, classic rock, progressive, folk, and others.
In recent years I (re)discovered long distance running, with emphasis on
development of a correct running form and technique. I also love basketball
and play it regularly.
I grew up in Petah
Tikva, Israel. This is a gray and generally uninspiring city not far from
Tel-Aviv. Still, it is my
hometown.
stuff