ETAPS 2019 (series) / TACAS 2019 (series) / TACAS 2019 /
Reachability Analysis for Termination and Confluence of Rewriting
In term rewriting, reachability analysis is concerned with the problem of deciding whether one term is reachable from another one by rewriting. Reachability analysis has several applications in termination and confluence analysis of rewrite systems. We give a unified view on reachability analysis for rewriting with and without conditions by means of what we call reachability logic. Moreover, we provide several techniques that fit into this general framework and can be efficiently implemented. The result is an increase in power of existing termination and confluence tools.
Mon 8 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 8 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 16:00 | |||
14:00 30mTalk | LCV: A Verification Tool for Linear Controller Software TACAS Junkil Park University of Pennsylvania, Miroslav Pajic Duke University, Oleg Sokolsky University of Pennsylvania, USA, Insup Lee Link to publication | ||
14:30 30mTalk | Semantic Fault Localization and Suspiciousness Ranking TACAS Maria Christakis MPI-SWS, Matthias Heizmann University of Freiburg, Muhammad Numair Mansur Max Planck Institute for Software Systems (MPI-SWS), Christian Schilling IST Austria, Valentin Wüstholz ConsenSys Diligence Link to publication | ||
15:00 30mTalk | Computing Coupled Similarity TACAS Link to publication | ||
15:30 30mTalk | Reachability Analysis for Termination and Confluence of Rewriting TACAS Link to publication | ||