Logic-Based Program Synthesis and Transformation 27th International Symposium, LOPSTR 2017, Namur, Belgium, October 10-12, 2017, Revised Selected Papers. Theoretical Computer Science and General Issues

This book constitutes the thoroughly refereed post-conference proceedings of the 27th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2017, held in Namur, Belgium, in October 2017. The 19 revised full papers were carefully reviewed and selected from 29 submissions. In addition to the 19 revised papers, this volume includes the abstracts of the invited talks by three outstanding speakers: Sumit Gulwani, Marieke Huisman, and Grigore Roşu. The aim of the LOPSTR series is to stimulate and promote international research and collaboration on logic-based program development. LOPSTR is open to contributions in all aspects of logic-based program development, all stages of the software life cycle, and issues of both programming-in-the-small and programming-in-the-large. LOPSTR traditionally solicits contributions, in any language paradigm, in the areas of synthesis, specification, transformation, analysis and verification, specialization, testing and certification, composition, program/model manipulation, optimization, transformational techniques in SE, inversion, applications, and tools. Front Matter ....Pages I-XVI Front Matter ....Pages 1-1 Generation of Initial Contexts for Effective Deadlock Detection (Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel)....Pages 3-19 A Rule-Based Approach to Analyzing Database Schema Objects with Datalog (Christiane Engels, Andreas Behrend, Stefan Brass)....Pages 20-36 Deadlock Detection of Java Bytecode (Cosimo Laneve, Abel Garcia)....Pages 37-53 Inferring Energy Bounds via Static Program Analysis and Evolutionary Modeling of Basic Blocks (Umer Liqat, Zorana Banković, Pedro Lopez-Garcia, Manuel V. Hermenegildo)....Pages 54-72 CARET Analysis of Multithreaded Programs (Huu-Vu Nguyen, Tayssir Touili)....Pages 73-90 Front Matter ....Pages 91-91 Context Generation from Formal Specifications for C Analysis Tools (Michele Alberti, Julien Signoles)....Pages 93-111 Liveness-Driven Random Program Generation (Gergö Barany)....Pages 112-127 Erlang Code Evolution Control (David Insa, Sergio Pérez, Josep Silva, Salvador Tamarit)....Pages 128-144 Front Matter ....Pages 145-145 Justifications in Constraint Handling Rules for Logical Retraction in Dynamic Algorithms (Thom Frühwirth)....Pages 147-163 Confluence and Convergence in Probabilistically Terminating Reduction Systems (Maja H. Kirkeby, Henning Christiansen)....Pages 164-179 Analysis of Rewriting-Based Systems as First-Order Theories (Salvador Lucas)....Pages 180-197 Front Matter ....Pages 199-199 A Constructor-Based Reachability Logic for Rewrite Theories (Stephen Skeirik, Andrei Stefanescu, José Meseguer)....Pages 201-217 Fuzzy Unification and Generalization of First-Order Terms over Similar Signatures (Hassan Aït-Kaci, Gabriella Pasi)....Pages 218-234 Nominal C-Unification (Mauricio Ayala-Rincón, Washington de Carvalho-Segundo, Maribel Fernández, Daniele Nantes-Sobrinho)....Pages 235-251 On Uniquely Closable and Uniquely Typable Skeletons of Lambda Terms (Olivier Bodini, Paul Tarau)....Pages 252-268 Front Matter ....Pages 269-269 A Certified Reference Validation Mechanism for the Permission Model of Android (Gustavo Betarte, Juan Campo, Felipe Gorostiaga, Carlos Luna)....Pages 271-288 Predicate Pairing with Abstraction for Relational Verification (Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti)....Pages 289-305 Variant-Based Decidable Satisfiability in Initial Algebras with Predicates (Raúl Gutiérrez, José Meseguer)....Pages 306-322 Combining Static and Dynamic Contract Checking for Curry (Michael Hanus)....Pages 323-340 Back Matter ....Pages 341-341