ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Wed 15 Apr 2015 15:30 - 16:00 at Skeel - Session 5 Chair(s): Jan Vitek

We prove that all valid Herbrand equalities can be inter-procedurally inferred for programs where all assignments are taken into account whose right-hand sides depend on at most one variable. The analysis is based on procedure summaries representing the weakest pre-conditions for finitely many generic post-conditions with template variables. In order to arrive at effective representations for all occurring weakest pre-conditions, we show for almost all values possibly computed at run-time, that they can be uniquely factorized into tree patterns and a terminating ground term. Moreover, we introduce an approximate notion of subsumption which is effectively decidable and ensures that finite conjunctions of equalities may not grow infinitely. Based on these technical results, we realize an effective fixpoint iteration to infer all inter-procedurally valid Herbrand equalities for these programs.

Wed 15 Apr

Displayed time zone: Azores change

14:00 - 16:00
Session 5ESOP at Skeel
Chair(s): Jan Vitek Northeastern University
14:00
30m
Talk
Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System
ESOP
Burke Fetscher Northwestern University, Koen Claessen Chalmers University of Technology, Michał Pałka Chalmers University of Technology, John Hughes Chalmers University of Technology, Robby Findler Northwestern University
14:30
30m
Talk
Refinement Types for Incremental Computational Complexity
ESOP
Ezgi Çiçek MPI-SWS, Deepak Garg MPI-SWS, Umut A. Acar Carnegie Mellon University
15:00
30m
Talk
Monotonic References for Efficient Gradual Typing
ESOP
Jeremy G. Siek Indiana University, Michael M. Vitousek Indiana University, Matteo Cimini Indiana University, Sam Tobin-Hochstadt Indiana University, Ronald Garcia University of British Columbia
15:30
30m
Talk
Inter-procedural Two-Variable Herbrand Equalities
ESOP
Stefan Schulze Frielinghaus Technische Universität München, Michael Petter Technische Universität München, Helmut Seidl Technische Universität München