dc.contributor.author
Singh, Gagandeep
dc.contributor.supervisor
Vechev, Martin
dc.contributor.supervisor
Püschel, Markus
dc.contributor.supervisor
Cousot, Patrick
dc.contributor.supervisor
Barrett, Clark
dc.date.accessioned
2020-10-14T12:12:54Z
dc.date.available
2020-10-14T10:49:54Z
dc.date.available
2020-10-14T12:12:54Z
dc.date.issued
2020
dc.identifier.uri
http://hdl.handle.net/20.500.11850/445921
dc.identifier.doi
10.3929/ethz-b-000445921
dc.description.abstract
With the widespread adoption of modern computing systems in different real-world applications such as autonomous vehicles, medical diagnosis, and aviation, it is critical to establish formal guarantees on their correctness before they are employed in the real-world. Automated formal reasoning about modern systems has been one of the core problems in computer science and has therefore attracted considerable interest from the research community. However, the problem has turned out to be quite challenging because of the ever-increasing scale, complexity, and diversity of these systems, which has so far limited the applicability of formal methods for their automated analysis. The central problem addressed in this dissertation is: are there generic methods for designing fast and precise automated reasoning for modern systems? We focus on two practically important problem domains: numerical software and deep learning models. We design new concepts, representations, and algorithms for providing the desired formal guarantees. We build our methodology on the elegant abstract interpretation framework for static analysis, which enables automated reasoning about infinite concrete behaviors with finite computable representations. Our methods are generic for the particular problem domain and allow precise analysis beyond the reach of prior work. For programs, we present a new theory of online decomposition that dynamically decomposes expensive computations, thereby reducing their complexity without any precision loss. Our theory is generic and can be used for decomposing all existing subpolyhedra domains without sacrificing precision. We leverage data-driven machine learning to further improve the performance of numerical program analysis without significant precision loss. For neural networks, we designed a new abstraction equipped with custom approximations of non-linearities commonly used in neural networks for fast and scalable analysis. We also created a new convex relaxations framework that produces more precise relaxations than possible with prior work. We provide a novel combination of our abstractions and relaxation framework with precise solvers, which enables state-of-the-art certification results. This thesis presents two new publicly available software systems: ELINA and ERAN. ELINA provides optimized implementations of the popular Polyhedra, Octagon, and Zone domain, based on our theory of online decomposition enabling fast and precise analysis of large Linux device drivers containing $>$ 500 variables in a few seconds. ERAN contains our custom abstraction, convex relaxation framework, and combination of relaxations with solvers for enabling fast and precise analysis of large neural networks, containing tens of thousands of neurons, within a few seconds. Both the systems were developed from scratch, and are currently state-of-the-art for their respective domains, producing results not possible with other competing systems.
en_US
dc.format
application/pdf
en_US
dc.language.iso
en
en_US
dc.publisher
ETH Zurich
en_US
dc.rights.uri
http://rightsstatements.org/page/InC-NC/1.0/
dc.subject
Program Analysis
en_US
dc.subject
Abstract Interpretation
en_US
dc.subject
Deep learning
en_US
dc.subject
Automated Formal Reasoning
en_US
dc.subject
Neural Network Verification
en_US
dc.title
Scalable Automated Reasoning for Programs and Deep Learning
en_US
dc.type
Doctoral Thesis
In Copyright - Non-Commercial Use Permitted
dc.date.published
2020-10-14
ethz.size
214 p.
en_US
ethz.code.ddc
DDC - DDC::0 - Computer science, information & general works::000 - Generalities, science
en_US
ethz.code.ddc
DDC - DDC::0 - Computer science, information & general works::080 - General collections
en_US
ethz.grant
Making Program Analysis Fast
en_US
ethz.identifier.diss
27096
en_US
ethz.publication.place
Zurich
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02664 - Inst. f. Programmiersprachen u. -systeme / Inst. Programming Languages and Systems::03948 - Vechev, Martin / Vechev, Martin
en_US
ethz.leitzahl.certified
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02664 - Inst. f. Programmiersprachen u. -systeme / Inst. Programming Languages and Systems::03948 - Vechev, Martin / Vechev, Martin
en_US
ethz.grant.agreementno
163117
ethz.grant.agreementno
163117
ethz.grant.fundername
SNF
ethz.grant.fundername
SNF
ethz.grant.funderDoi
10.13039/501100001711
ethz.grant.funderDoi
10.13039/501100001711
ethz.grant.program
Projekte MINT
ethz.relation.hasPart
20.500.11850/129815
ethz.relation.hasPart
20.500.11850/390875
ethz.relation.hasPart
20.500.11850/314006
ethz.relation.hasPart
10.3929/ethz-b-000390873
ethz.relation.hasPart
20.500.11850/314007
ethz.relation.hasPart
handle/20.500.11850/430024
ethz.date.deposited
2020-10-14T10:50:04Z
ethz.source
FORM
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2020-10-14T12:13:50Z
ethz.rosetta.lastUpdated
2022-03-29T03:30:57Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&amp;rft_val_fmt=info:ofi/fmt:kev:mtx:journal&amp;rft.atitle=Scalable%20Automated%20Reasoning%20for%20Programs%20and%20Deep%20Learning&amp;rft.date=2020&amp;rft.au=Singh,%20Gagandeep&amp;rft.genre=unknown&amp;rft.btitle=Scalable%20Automated%20Reasoning%20for%20Programs%20and%20Deep%20Learning
﻿ Search print copy at ETH Library