TY - GEN
T1 - Inter-procedural two-variable Herbrand equalities
AU - Frielinghaus, Stefan Schulze
AU - Petter, Michael
AU - Seidl, Helmut
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2015.
PY - 2015
Y1 - 2015
N2 - We prove that all valid Herbrand equalities can be interprocedurally 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 preconditions 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 interprocedurally valid Herbrand equalities for these programs.
AB - We prove that all valid Herbrand equalities can be interprocedurally 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 preconditions 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 interprocedurally valid Herbrand equalities for these programs.
UR - http://www.scopus.com/inward/record.url?scp=84926635263&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-46669-8_19
DO - 10.1007/978-3-662-46669-8_19
M3 - Conference contribution
AN - SCOPUS:84926635263
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 457
EP - 482
BT - Programming Languages and Systems - 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings
A2 - Vitek, Jan
PB - Springer Verlag
T2 - 24th European Symposium on Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
Y2 - 11 April 2015 through 18 April 2015
ER -