Selected and Extended Papers from TACAS 2018: Preface
- PDF / 172,176 Bytes
- 2 Pages / 439.37 x 666.142 pts Page_size
- 92 Downloads / 184 Views
Selected and Extended Papers from TACAS 2018: Preface Dirk Beyer1
· Marieke Huisman2
Received: 25 June 2020 / Accepted: 11 July 2020 / Published online: 24 September 2020 © The Author(s) 2020
TACAS 2018, the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems took place in Thessaloniki, Greece on April 16–20, 2018, as part of the European Joint Conferences on Theory and Practice of Software (ETAPS). TACAS is a forum for researchers, developers, and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The conference aims to bridge the gaps between different communities with this common interest and to support them in their quest to improve the utility, reliability, flexibility, and efficiency of tools and algorithms for building systems. This special issue of the Journal of Automated Reasoning contains revised and extended versions of seven papers selected out of 45 papers presented at the conference. The papers that were selected for this special issue all provide new theoretical contributions to the construction and analysis of systems. In addition to this special issue, a companion special issue for TACAS 2018 appears in the journal Software Tools for Technology Transfer (STTT), containing selected papers that report on advances in tools and tool sets in this area. All selected papers underwent a thorough reviewing process, with several iterations, where each paper was reviewed by several external domain experts. As a result of this selection process, this special issue contains the following papers. Kshitij Bansal, Eric Koskinen, and Omer Tripp propose an algorithm to reason automatically about commutativity (and non-commutativity) conditions for method pairs in a parallel context. They illustrate their approach by synthesizing commutativity conditions for several widely used data structures. Randal E. Bryant introduces chain reduction to enable reduced ordered binary decision diagrams (BDDs) and zero-suppressed binary decision diagrams (ZDDs) to each take advantage of the others’ ability to symbolically represent Boolean functions in a compact form. He proposes extensions to the standard algorithms for operating on BDDs and ZDDs that enable them to operate on the chain-reduced versions.
B B
Dirk Beyer [email protected] https://www.sosy-lab.org/people/beyer/ Marieke Huisman [email protected] https://wwwhome.ewi.utwente.nl/~marieke/
1
LMU Munich, Oettingenstr. 67, 80538 Munich, Germany
2
University of Twente, P.O. Box 217, 7500 AE Enschede, The Netherlands
123
1332
D. Beyer, M. Huisman
Adrien Champion, Tomoya Chiba, Naoki Kobayashi, and Ryosuke Sato propose an extension of the ICE framework for automatically finding refinement types of higher-order function programs. The key idea of their approach is that the generated implication constraints can be generalized to find invariants of recursive functions with multiple function calls. Peter Chini, Roland Meyer, and Prakash Saivasan study the fine-gr
Data Loading...