Project

Back to overview

Making Program Analysis Fast

Applicant Vechev Martin
Number 163117
Funding scheme Project funding
Research institution Professur für Informatik ETH Zürich
Institution of higher education ETH Zurich - ETHZ
Main discipline Information Technology
Start/End 01.10.2015 - 30.11.2018
Approved amount 345'016.00
Show all

Keywords (4)

static analysis; numerical abstract domains; performance; optimizations

Lay Summary (German)

Lead
Beschleunigung von Programmanalyse
Lay summary

Computer sind ein fester Bestandteil unseres Lebens und revolutionierten die Art, wie wir mit der Welt interagieren und kommunizieren. Von der Simulation komplexer physikalischer und biologischer Systeme, bis hin zur Ermöglichung   leistungsfähiger Smartphones, spielt EDV eine grundlegende Rolle in der modernen Gesellschaft. Dennoch ist das Programmieren dieser Computer immer noch eine schwierige, zeitaufwändige und fehleranfällige Tätigkeit. Deshalb bleibt die Sicherstellung von Programmkorrektheit und -effizienz ein grundlegendes Problem der Informatik.

Dadurch, dass Programme grösser und komplexer werden hat sich insbesondere der Bedarf an „Automated Reasoning Tools“ und Techniken, welche dafür sorgen, dass Programme sich so verhalten wie sie sollen, drastisch erhöht.

 Wegen dem Bedarf an derart automatisierten Techniken waren in den letzten zehn Jahren enorme Fortschritte bei Werkzeugen für Programmanalyse zu sehen. Techniken, die einst als rein theoretisch galten wurden verbessert und werden nun in komplexen realen Situationen angewendet, unter anderem bei Gerätetreibern oder in grossem Umfang für sicherheitsrelevante Systeme wie Flugsteuerungssoftware.

 Das Hauptziel des Projektes ist es, neue Algorithmen, Datenstrukturen und Techniken zu entwickeln, welche die Programmanalyse signifikant beschleunigen. Auf diese Weise wird die Lücke zwischen Analysekosten und Aussagekraft geschlossen, sodass Programme, die bisher nicht in einem vernünftigen Zeitrahmen analysiert werden konnten für Analyse und Verifikation zugänglich werden.

 Unser allgemeiner Ansatz ist dabei der Transfer von Leistungsoptimierungstechniken aus dem Gebiet des High Performance Computings in die Programmanalyse. Dies beinhaltet insbesondere die Entwicklung von architekturbewusster Optimierungen, Autotuning und Programmgeneratoren für die Programmanalyse

Direct link to Lay Summary Last update: 20.10.2015

Responsible applicant and co-applicants

Employees

Publications

Publication
An abstract domain for certifiying neural networks
SinghGagandeep, GehrT., PüschelM., VechevMartin (2019), An abstract domain for certifiying neural networks, in ACM Program. Lang., 3(41), 1-30.
A practical construction for decomposing numerical abstract domains
SinghGagandeep, GehrT., PüschelM., VechevMartin (2018), A practical construction for decomposing numerical abstract domains, in ACM Program , 2(55), 1-28.
Fast and effective robustness certification
Singh Gagandeep, GehrT., MirmanM., PüschelM., VechevMartin (2018), Fast and effective robustness certification, in Advances in neural Information Processing Systems, 10825-10836.
Fast numerical program analysis with reinforcement learning
Singh Gagandeep, PüschelM., VechevMartin (2018), Fast numerical program analysis with reinforcement learning, in Computer Aided Verification, 211-229.
Fast polyhedra abstract domain
Singh Gagandeep, PüschelM., VechevMartin (2017), Fast polyhedra abstract domain, in Proc. principles of Programming Languages, 46-59.

Awards

Title Year
IBM PhD fellowship 2019

Abstract

Computers have become an integral part of our lives and have revolutionized the way weinteract and communicate with the world. From simulating complex physical and biologicalsystems to enabling powerful smart phones, computing plays a fundamental role in modernsociety. However, programming those computers is still a difficult, time-consuming, anderror-prone activity. Thus, ensuring that programs work correctly and efficiently remainsa fundamental problem in computer science. In particular, as programs grow larger andmore complex, the need for automated reasoning tools and techniques that can ensure thatprograms behave as they are supposed to, has increased dramatically. Because of the needfor such automated techniques, the last decade has seen tremendous progress in softwareanalysis tools. Techniques once considered purely theoretical have been improved [13, 24]and are now applied in complex real world settings including device drivers [2] or largescalesafety critical systems such as flight control software [6].A fundamental challenge in developing automated reasoning enginesis striking a careful balance between cost (both space and time) and the expressive powerof the analysis engine (precision). Achieving this balance is critical: an analyzer that is tooimprecise can fail to verify correct programs, while an analyzer which is very precise can betoo costly (e.g., run out of memory or require weeks to finish) to be useful for real worldprograms.The main goal of this proposal is to develop new algorithms, data structures,and techniques that significantly speed up program analysis. This way, we bridge the gapbetween analysis cost and expressiveness and programs that previously could not be analyzedin a reasonable time frame become amenable to analysis and verification. Our highlevel approach is to import performance optimization techniques that were developed in thedistinct domain of high performance computing to program analysis. Specifically this includesthe development of architecture-cognizant optimizations, autotuning, and programgenerators for program analysis.Our proposal is inter-disciplinary: to make progress weneed to combines ideas from two distinct areas of computer science: high performancealgorithms and optimizations (represented by Prof. Dr. Markus P¨uschel) and programanalysis and verification (represented by Prof. Dr. Martin Vechev). Our preliminary results(described later) have been highly encouraging: in a recent paper on the subject [44] (aboutto appear), we show in many cases almost an order of magnitude speed-up compared to(already optimized) analysis engines. We believe that our proposal can have significantimpact on both the algorithmic side but also in terms of practical tools to be released andadopted by the research community and by industry.
-