The International Symposium on Logic-based Program Synthesis and Transformation LOPSTR annually gathers researchers interested in logic-based program development.The LOPSTR series stimulates and promotes international research and collaboration in all aspects of the field, covering all stages of the software life cycle and addressing issues related to both programming-in-the-small and programming-in-the-large.This special issue contains the revised and extended versions of selected papers presented at the 32nd International Symposium on Logic-Based Program Synthesis and Transformation LOPSTR 2022 which was hosted by the Tbilisi State University, Georgia, from September 6 to September 8, 2022.The authors of selected papers were invited to submit an improved, extended version to this special issue of Fundamenta Informaticae.The papers they submitted went through a careful review by qualified international referees, to whom we express our deep gratitude.

In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KERNELC, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KERNELC in the 𝕂 semantic framework, we enrich the symbolic execution facilities recently provided by 𝕂 with novel capabilities for contract synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that axiomatically explains the execution of any (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KINDSPEC 2.1, which generates logical axioms that express pre- and post-condition assertions which define the precise input/output behavior of the C routines. Thanks to the integrated support for symbolic execution and deductive verification provided by 𝕂, some synthesized axioms that cannot be guaranteed to be correct by construction due to abstraction can finally be verified in our setting with little effort.

Abstract The timed concurrent constraint language (tccp) is a timed extension of the concurrent constraint paradigm.tccpwas defined to model reactive systems, where infinite behaviors arise naturally. In previous works, a semantic framework and abstract diagnosis method for the language have been defined. On the basis of that semantic framework, this paper proposes an abstract semantics that, together with a widening operator, is suitable for the definition of different analyses fortccpprograms. The abstract semantics is correct and can be represented as a finite graph where each node represents a hypothetical (abstract) computational step of the program. The widening operator allows us to guarantee the convergence of the abstract fixpoint computation.

Abstract Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which represents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and sometimes the needed fragment is quite huge. In this work, we provide an alternative automatic decision method to check whether a given property, specified in a linear temporal logic, isvalidw.r.t. atccpprogram. Our proposal (based on abstract interpretation techniques) does not require to build any model at all. Our results guarantee correctness but, as usual when using an abstract semantics, completeness is lost.

Formal specifications can be used for various software engineering activities ranging from finding errors to documenting software and automatic test-case generation. Automatically discovering specifications for heap-manipulating programs is a challenging task. In this paper, we propose a technique for automatically inferring formal specifications from C code which is based on the symbolic execution and automated reasoning tandem "Matching Logic/K framework". We implemented our technique for a fragment of C called KernelC, in the automated tool KingSpec, which generates axioms that describe the precise input/output behavior of C routines that handle pointer-based structures, i.e., result values and state change. These specifications can be written either in Matching Logic itself, which is useful for further automated analysis within the K formal environment, or in sugared axiomatic form, which favors better human inspection. Since we rely on rewriting logic K semantics specification of programming languages, our approach can be easily extended to any language for which %that a formal semantics in K is given.

This paper presents a technique to automatically infer algebraic property-oriented specifications from first-order Curry programs. Curry is a lazy functional logic language and the interaction between laziness and logical variables raises some additional difficulties with respect to other proposals for functional languages. Our technique statically infers from the source code of a Curry program a specification which consists of a set of equations relating (nested) operation calls that have the same behavior. We propose a (glass-box) semantic-based inference method which relies on a fully-abstract (condensed) semantics for achieving, to some extent, the correctness of the inferred specification, differently from other (black-box) approaches based on testing techniques.

Abstract The timed concurrent constraint language (tccp in short) is a concurrent logic language based on the simple but powerful concurrent constraint paradigm of Saraswat. In this paradigm, the notion of store-as-value is replaced by the notion of store-as-constraint, which introduces some differences w.r.t. other approaches to concurrency. In this paper, we provide a general framework for the debugging of tccp programs. To this end, we first present a new compact, bottom-up semantics for the language that is well suited for debugging and verification purposes in the context of reactive systems. We also provide an abstract semantics that allows us to effectively implement debugging algorithms based on abstract interpretation. Given a tccp program and a behavior specification, our debugging approach automatically detects whether the program satisfies the specification. This differs from other semi-automatic approaches to debugging and avoids the need to provide symptoms in advance. We show the efficacy of our approach by introducing two illustrative examples. We choose a specific abstract domain and show how we can detect that a program is erroneous.

This book discusses four approaches typically used for the verification of reactive systems.However, the book is not merely a description of these four formalisms, since the existing connections between these techniques are also established.In addition, complexity results associated with each method are presented, together with discussions about good features and difficulties that must be faced when dealing with each particular technique.It cannot be said that this is a practical book.On the contrary, this book presents fundamental theory that every researcher on formal methods should be familiar with.Therefore, the audience for this book is mainly theoreticians with some background in automata theory and logics.They will enjoy discovering the underlying interrelations among the different approaches presented along the book.Almost all the results presented encompass useful descriptions and explanations, which makes the reading more fluent, especially when the reader doesn't want to go into the details of a specific proof or result.It must be said that the notation used by the authors does not always follow the established notation, as used in the original research papers, for instance.This fact increases the difficulty of reading the text since some extra time must be invested in getting accustomed to the new notation.Independently from the contents, the readability of the book is sometimes degraded due to the presence of some typographical errors, but they do not prevent the reader from understanding the topics of the text.Looking into the contents, the book starts with a marvelous introduction where, first of all, a classification of formal methods and systems can be found.The ancient (maybe not so ancient) history of logic theories and verification techniques is narrated.This part of the book, in addition to being a very nice introductory description of the formalisms that will be described in the rest of the book, is also an advertisement to the reader of the theoretical point of view that will be used through the book, which continuously will frame the equivalences and relations among the four formalisms.The book includes a remarkable bibliography section.This is not only notable for its contents, but also for how they are cited.Bibliographic references are perfectly integrated into the book itself, and can be especially useful in the introduction and in the appendixes, where the topics are not completely developed and the reader is referred to related and perhaps more detailed works.Before considering the main contents of the book, the second chapter presents a unified specification language which combines µ-calculus, ω-automata, temporal logics and predicate logics.This unified language provides the author with an unified notation for defining each formalism in the rest of the book and for showing the formal links between the different approaches.Notions such as Kripke structures, fairness, simulations, bisimulations and products of structures are introduced and will be used in several sections of the book.The organization of the main chapters of the book is as follows: Chapter 3 is devoted to the first formalism, the µ-calculus; then, Chapter 4 deals with ω-automata, the following chapter describes temporal logics (in particular, variants of CTL) and finally, in Chapter 6, predicate logics are used for the verification of reactive systems.Note that although these four chapters

The language Timed Concurrent Constraint (tccp) is the extension over time of the Concurrent Constraint Programming (cc) paradigm that allows us to specify concurrent systems where timing is critical, for example reactive systems. Systems which may have an infinite number of states can be specified in tccp. Model checking is a technique which is able to verify finite-state systems with a huge number of states in an automatic way. In the last years several studies have investigated how to extend model checking techniques to systems with an infinite number of states. In this paper we propose an approach which exploits the computation model of tccp. Constraint based computations allow us to define a methodology for applying a model checking algorithm to (a class of) infinite-state systems. We extend the classical algorithm of model checking for LTL to a specific logic defined for the verification of tccp and to the tccp Structure which we define in this work for modeling the program behavior. We define a restriction on the time in order to get a finite model and then we develop some illustrative examples. To the best of our knowledge this is the first approach that defines a model checking methodology for tccp.