Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Wed 16 Jan 2019 16:05 - 16:27 at Sala I - Machine Learning and Linear Algebra Chair(s): Aws Albarghouthi

This paper investigates the problem of reasoning about non-linear behavior of simple numerical loops. Our approach builds on classical techniques for analyzing the behavior of linear dynamical systems. It is well-known that a closed-form representation of the behavior of a linear dynamical system can always be expressed using algebraic numbers, but such an approach can create formulas that present an obstacle for automated-reasoning tools. This paper characterizes when linear loops have closed forms in simpler theories that are more amenable to automated reasoning. The algorithms for computing closed forms described in the paper avoid the use of algebraic numbers, and produce closed forms expressed using polynomials and exponentials over rational numbers. We show that the logic for expressing closed forms is decidable, yielding decision procedures for verifying safety and termination of a class of numerical loops over rational numbers. We also show that the procedure for computing closed forms for this class of numerical loops can be used to over-approximate the behavior of arbitrary numerical programs (with unrestricted control flow, non-deterministic assignments, and recursive procedures).

Slides (slides.pdf)243KiB

Wed 16 Jan

Displayed time zone: Belfast change

15:21 - 16:27
Machine Learning and Linear AlgebraResearch Papers at Sala I
Chair(s): Aws Albarghouthi University of Wisconsin-Madison
15:21
22m
Talk
code2vec: Learning Distributed Representations of Code
Research Papers
Uri Alon Technion, Meital Zilberstein Technion, Omer Levy University of Washington, USA, Eran Yahav Technion
Link to publication DOI Pre-print Media Attached File Attached
15:43
22m
Talk
An Abstract Domain for Certifying Neural Networks
Research Papers
Link to publication DOI Media Attached
16:05
22m
Talk
Closed Forms for Numerical Loops
Research Papers
Zachary Kincaid Princeton University, Jason Breck University of Wisconsin - Madison, John Cyphert University of Wisconsin - Madison, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc.
Link to publication DOI Media Attached File Attached