This article presents an Event-B model and an interactive GUI prototype for an air traffic control system called the arrival manager (AMAN). AMAN is a safety-critical interactive system designed for air traffic controllers to manage landings at an airport. The presented formal model consists of a human-machine interface comprising interactive and autonomous parts. Safety properties of the system were proven using the Rodin platform, while validation was carried out using the ProB tool. We turned the formal model into an executable AMAN prototype by combining interactive domain-specific visualizations and automatic simulation using the VisB and SimB components of ProB . We used validation obligations (VOs) to systematically validate the model’s and the prototype’s compliance with the requirements and uncovered some contradictions and ambiguities in the case study.

Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.

The B method is a formal method supported by a variety of tools. Those tools, like any complex piece of software, may suffer from performance issues and vulnerabilities. In this work, we leverage performance fuzzing to generate inputs that uncover potential performance issues in the ProB model checker and its employed constraint solving backends. These backends include a mix of constraint solvers that are directly implemented in ProB or are bindings to third-party solvers such as Z3. During constraint solving, any such backend can be selected to solve a given constraint. As performance fuzzing algorithm, we utilise BanditFuzz. BanditFuzz utilises two multi-armed bandit agents to control a fuzz generator and mutator. This way, the algorithm can generate targeted input benchmarks that are well-formed inputs to ProB yet exhibit significant performance differences between the employed constraint solvers. We describe how we adapted BanditFuzz for the B method, what differences exist to the original implementation for the SMT-LIB standard, and how we ensure well-definedness of the randomly generated benchmarks. Further, we consider two opposed approaches to integrate BanditFuzz with ProB : as an external tool that considers ProB as a black box, and as an internal tool that has direct dependency onto ProB ’s source code and can capitalise on available, internal functionalities. Our experiments successfully uncovered performance issues in specific backends and even external tooling, providing valuable insights into areas that required improvement. Ultimately, we conclude that BanditFuzz is a valuable tool for development and advocate for the external architecture, as its benefits outweigh the drawbacks.

Certified control makes it possible to use artificial intelligence for safety-critical systems. It is a runtime monitoring architecture, which requires an AI to provide certificates for its decisions; these certificates can then be checked by a separate classical system. In this article, we evaluate the practicality of certified control for providing formal guarantees about an AI-based perception system. In this case study, we implemented a certificate checker that uses classical computer vision algorithms to verify railway signs detected by an AI object detection model. We have integrated this prototype with the popular object detection model YOLO. Performance metrics on generated data are promising for the use-case, but further research is needed to generalize certified control for other tasks.

Abstract We present a new SAT backend for the B-Method to enable new applications of formal methods. The new backend interleaves low-level SAT solving with high-level constraint solving. It provides a “bare metal” access to SAT solving, while pre- and post-calculations can be done in the full B language, with access to higher-order or even infinite data values. The backend is integrated into ProB, not as a general purpose backend, but as a dedicated backend for solving hard constraint satisfaction and optimisation problems on complex data. In the article we present the approach, its origin in the proof of Cook’s theorem, and illustrate and evaluate it on a few novel applications of formal methods, ranging from biology to railway applications.

Refinement guarantees that the concrete version of a model does not violate the constraints introduced at the abstract level. The peculiarity of refinement, however, is that we have no guarantee about the preservation of the behavior of the model. For example, a trace (a set of desirable states and transitions) created on the abstract model may not replay on the concrete model. Its manual recreation, usually via animation, is necessary to run the trace, as the model may have changed significantly during refinement. However, this is a labor-intensive and error-prone task. To this end, this article presents an automatic trace refining technique and tool called BERT (B and Event-B Trace Refinement Technique) that allows modelers to ensure the behavioral integrity of high-level traces at the concrete level. The cost- and time-effectiveness of BERT are shown in industrial-strength case studies from the automotive and aviation domains.

Abstract Especially in industrial applications of formal modeling, validation is as important as verification. Thus, it is important to integrate the stakeholders’ and the domain experts’ feedback as early as possible. In this work, we propose two approaches to enable this: (1) a static export of an animation trace into a single HTML file, and (2) a dynamic export of a classical B model as an interactive HTML document, both based on domain-specific visualizations. For the second approach, we extend the high-level code generator B2Program by JavaScript and integrate VisB visualizations alongside SimB simulations with timing, probabilistic and interactive elements. An important aspect of this work is to ease communication between modelers and domain experts. This is achieved by implementing features to run simulations, sharing animated traces with descriptions and giving feedback to each other. This work also evaluates the performance of the generated JavaScript code compared with existing approaches with Java and C++ code generation as well as the animator, constraint solver, and model checker ProB.

Abstract ProBprovides a constraint solver for the B-method written in Prolog and can make use of different backends based on SAT and SMT solving. One such backend translates B and Event-B operators to SMT-LIB using the Z3 solver. This translation uses quantifiers to axiomatize some operators, which are not well-handled by Z3. Several relational constraints such as the transitive closure are not supported by this translation. In this article, we substantially improve the translation to SMT-LIB by employing a more constructive rather than axiomatized style using Z3’s lambda function. Thereby, we are able both to translate more B and Event-B operators to SMT-LIB and improve the overall performance. We further extendProB’s interface to Z3 to run different solver configurations in parallel. In addition, we present a direct implementation of SMT solving in Prolog usingProB’s constraint solver as a theory solver. We hereby aim to combine the strengths of conflict-driven clause learning for identifying contradictions withProB’s constraint solver for finding solutions. We deem this implementation to be worthwhile sinceProB’s constraint solver is tailored toward solving B and Event-B constraints, and we herewith avoid the dependency on an external SMT solver. Empirical results show that the new integration of Z3 has improved performance of constraint solving and enables to solve several constraints which cannot be solved byProB’s constraint solver. Furthermore, the direct implementation of SMT solving inProBshows benefits compared toProB’s constraint solver and the integration of Z3.

Abstract Even though the core of the Prolog programming language has been standardized by ISO since 1995, it remains difficult to write complex Prolog programs that can run unmodified on multiple Prolog implementations. Indeed, implementations sometimes deviate from the ISO standard and the standard itself fails to cover many features that are essential in practice. Most Prolog applications thus have to rely on nonstandard features, often making them dependent on one particular Prolog implementation and incompatible with others. We examine one such Prolog application: ProB, which has been developed for over 20 years in SICStus Prolog. The article describes how we managed to refactor the codebase of ProB to also support SWI-Prolog, with the goal of verifying ProB’s results using two independent toolchains. This required a multitude of adjustments, ranging from extending the SICStus emulation in SWI-Prolog on to better modularizing the monolithic ProB codebase. We also describe notable compatibility issues and other differences that we encountered in the process, and how we were able to deal with them with few major code changes.

Abstract Both logic programming in general and Prolog in particular have a long and fascinating history, intermingled with that of many disciplines they inherited from or catalyzed. A large body of research has been gathered over the last 50 years, supported by many Prolog implementations. Many implementations are still actively developed, while new ones keep appearing. Often, the features added by different systems were motivated by the interdisciplinary needs of programmers and implementors, yielding systems that, while sharing the “classic” core language, in particular, the main aspects of the ISO-Prolog standard, also depart from each other in other aspects. This obviously poses challenges for code portability. The field has also inspired many related, but quite different languages that have created their own communities. This article aims at integrating and applying the main lessons learned in the process of evolution of Prolog. It is structured into three major parts. First, we overview the evolution of Prolog systems and the community approximately up to the ISO standard, considering both the main historic developments and the motivations behind several Prolog implementations, as well as other logic programming languages influenced by Prolog. Then, we discuss the Prolog implementations that are most active after the appearance of the standard: their visions, goals, commonalities, and incompatibilities. Finally, we perform a SWOT analysis in order to better identify the potential of Prolog and propose future directions along with which Prolog might continue to add useful features, interfaces, libraries, and tools, while at the same time improving compatibility between implementations.

Abstract The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an appropriate level of certainty is reached, code generators are used in order to gain executable code. In this paper, we propose a different approach: instead of generating code from formal models, it is also possible to embed a model checker or animator into applications in order to use the formal models themselves at runtime. We present a Java API to the ProB animator and model checker. We describe several case studies that use this API as enabling technology to interact with a formal specification at runtime.

Abstract In this article, we present a concrete realisation of the ETCS hybrid level 3 concept, whose practical viability was evaluated in a field demonstration in 2017. Hybrid level 3 introduces virtual subsections as sub-divisions of classical track sections with trackside train detection. Our approach introduces an add-on for the radio block centre (RBC) of Thales, called virtual block function (VBF), which computes the occupation states of the virtual subsections using the train position reports, train integrity information, and the track occupation states. From the perspective of the RBC, the VBF behaves as an interlocking that transmits all signal aspects for virtual signals introduced for each virtual subsection to the RBC. We report on the development of the VBF, implemented as a formal B model executed at runtime using ProB and successfully used in a field demonstration to control real trains.

Algebraic State-Transition Diagrams (ASTDs) are extensions of common automata and statecharts that can be combined with process algebra operators like sequence, choice, guard and quantified synchronization. They were previously introduced for the graphical representation, specification and proof of information systems. In an attempt to use ASTDs to specify cyber-attack detection, we have identified a number of missing features in ASTDs. This paper extends the ASTD notation with state variables (attributes), actions on transitions, and a new operator called flow which corresponds to AND states in statecharts and is a compromise between interleaving and synchronization in process algebras. We provide a formal structured operational semantics of these extensions and illustrate its implementation in an OCaml-based interpreter called iASTD and the model checker ProB. Extended ASTDs are illustrated in a case study in cyber attack detection.

Abstract Constraint satisfaction problems can be expressed very elegantly in state-based formal methods such as B. But can such specifications be directly used for solving real-life problems? In other words, can a formal model be more than a design artefact but also be used at runtime for inference and problem solving? We will try and answer this important question in the present paper with regard to the university timetabling problem. We report on an ongoing project to build a curriculum timetable validation tool where we use a formal model as the basis to validate timetables from a student’s perspective and to support incremental modification of timetables. In this article we describe the problem domain, the formalization in B and our approach to execute the formal model in a production system using ProB .

We present an integration of the constraint solving kernel of the ProB model checker with the SMT solver Z3. We apply the combined solver to B and Event-B predicates, featuring higher-order datatypes and constructs like set comprehensions. To do so we rely on the finite set logic of Z3 and provide a new translation from B to Z3, better suited for constraint solving. Predicates can then be solved by the two solvers working hand in hand: constraints are set up in both solvers simultaneously and (intermediate) results are transferred. We thus combine a constraint logic programming based solver with a DPLL(T) based solver into a single procedure. The improved constraint solver finds application in many validation tasks, from animation of implicit specifications, to test case generation, bounded and symbolic model checking on to disproving of proof obligations. We conclude with an empirical evaluation of our approach focusing on two dimensions: comparing low and high-level encodings of B as well as comparing pure ProB to ProB combined with Z3.

Abstract Partial order reduction has been very successful at combatting the state explosion problem for lower-level formalisms, but has thus far made hardly any impact for model checking higher-level formalisms such as B, Z or TLA + . This paper attempts to remedy this issue in the context of Event-B, with its much more fine-grained events and thus increased potential for event-independence and partial order reduction. In this work, we provide a detailed description of a partial order reduction for explicit state model checking in ProB. The technique is evaluated on a variety of models. The implementation of the method is discussed, which is based on new constraint-based analyses. Further, we give a comprehensive description for elaborating the implementation into the LTL model checker of ProB for checking LTL − X formulae.

The 30th edition of the International Conference of Logic Programming took place in Vienna in July 2014 at the Vienna Summer of Logic - the largest scientific conference in the history of logic. Following the initiative in 2010 taken by the Association for Logic Programming and Cambridge University Press, the full papers accepted for the International Conference on Logic Programming again appear as a special issue of Theory and Practice of Logic Programming (TPLP) - the 30th International Conference on Logic Programming Special Issue. Papers describing original, previously unpublished research and not simultaneously submitted for publication elsewhere were solicited in all areas of logic programming including but not restricted to: Theory: Semantic Foundations, Formalisms, Non- monotonic Reasoning, Knowledge Representation; Implementation: Compilation, Memory Management, Virtual Machines, Parallelism; Environments: Program Analysis, Transformation, Validation, Verification, Debugging, Profiling, Testing; Language Issues: Concurrency, Objects, Coordination, Mobility, Higher Order, Types, Modes, Assertions, Programming Techniques; Related Paradigms: Abductive Logic Programming, Inductive Logic Programming, Constraint Logic Programming, Answer-Set Programming; Applications: Databases, Data Integration and Federation, Software Engineering, Natural Language Processing, Web and Semantic Web, Agents, Artificial Intelligence, Bioinformatics.

Abstract The Event-B method can be used to model all sorts of discrete event systems, among them sequential programs. In this article we describe our experiences with using Event-B by way of two examples. We present a simple model of a factorial program, explaining the method, and a more intricate model of the Quicksort algorithm, providing some insights into strengths and weaknesses of Event-B. The two models are interspersed with our observations and some suggestions of how, we believe, Event-B could evolve. This evaluation of Event-B is intended to serve for determining directions for the evolution of Event-B and judging progress. It is our hope that the observations and suggestions can also be put to use for similar modelling formalisms, such as Z, ASM or VDM.

The performance of many dynamic language implementations suffers from high allocation rates and runtime type checks. This makes dynamic languages less applicable to purely algorithmic problems, despite their growing popularity. In this paper we present a simple compiler optimization based on online partial evaluation to remove object allocations and runtime type checks in the context of a tracing JIT. We evaluate the optimization using a Python VM and find that it gives good results for all our (real-life) benchmarks.

Abstract In this paper we describe the successful application of the ProB tool for data validation in several industrial applications. The initial case study centred on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for Atelier B. Atelier B, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense, and they need to be revalidated whenever the rail network infrastructure changes. In this paper we show how we were able to use ProB to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in a few minutes that were manually uncovered in about one man-month. We have repeated this task for three ongoing projects at Siemens, notably the ongoing automatisation of the line 1 of the Paris Métro. Here again, about a man month of effort has been replaced by a few minutes of computation. This achievement required the extension of the ProB kernel for large sets as well as an improved constraint propagation algorithm. We also outline some of the effort and features that were required in moving from a tool capable of dealing with medium-sized examples towards a tool able to deal with actual industrial specifications. We also describe the issue of validating ProB , so that it can be integrated into the SIL4 development chain at Siemens.

Abstract Initially, the Rodin platform for Event‐B did away with a textual representation for models. In this paper, we explain why a textual representation was required after all and we present the semantic‐aware text editor Camille for Rodin. We explain the design choices of Camille, such as splitting the syntax into two‐levels for machine and formula syntax. We also describe the challenges, such as synchronizing the textual representation with the Rodin database, and how they were overcome using an EMF abstraction layer. Copyright © 2011 John Wiley & Sons, Ltd.

Abstract Establishing the absence of deadlocks is important in many applications of formal methods. The use of model checking for finding deadlocks in formal models is often limited. In this paper, we propose a constraint-based approach to finding deadlocks employing the ProB constraint solver. We present the general technique, as well as various improvements that had to be performed on ProB's Prolog kernel, such as reification of membership and arithmetic constraints. This work was guided by an industrial case study, where a team from Bosch was modelling a cruise control system. Within this case study, ProB was able to quickly find counterexamples to very large deadlock-freedom constraints. In the paper, we also present other successful applications of this new technique. Experiments using SAT and SMT solvers on these constraints were thus far unsuccessful.

Most Prolog implementations are implemented in low-level languages such as C and are based on a variation of the WAM instruction set, which enhances their performance but makes them hard to write. In addition, many of the more dynamic features of Prolog (like assert), despite their popularity, are not well supported. We present a high-level continuation-based Prolog interpreter based on the PyPy project. The PyPy project makes it possible to easily and efficiently implement dynamic languages. It provides tools that automatically generate a just-in-time compiler for a given interpreter of the target language, by using partial evaluation techniques. The resulting Prolog implementation is surprisingly efficient: it clearly outperforms existing interpreters of Prolog in high-level languages such as Java. Moreover, on some benchmarks, our system outperforms state-of-the-art WAM-based Prolog implementations. Our paper aims to show that declarative languages such as Prolog can indeed benefit from having a just-in-time compiler and that PyPy can form the basis for implementing programming languages other than Python.

Visualizing, e.g., the structure of a large software project, as a graph can be very confusing and ineffective. The reason can be the presence of countless overlapping arrows, which make a graph unclear and difficult to be interpreted by a human. To deal with this problem, we propose a new data visualization, namely pie tree visualization, which we illustrate on the architecture of a real-life example from the deploy project.

This paper describes SOC, a program slicer for CSP specifications. In order to increase the precision of program slicing, SOC uses a new data structure called Context-sensitive Synchronized Control Flow Graph (CSCFG). Given a CSP specification, SOC generates its associated CSCFG and produces from it two different kinds of slices; which correspond to two different static analyses. We present the tool's architecture, its main applications and the results obtained from experiments conducted in order to measure the performance of the tool.

This paper summarises roughly ten years of experience using declarative programming for developing tools to validate formal specifications. More precisely, we present insights gained and lessons learned while implementing animators and model checkers in Prolog for various specification languages, ranging from process algebras such as CSP to model-based specifications such as Z and B.

Symmetry reduction holds great promise to counter the state explosion problem. However, currently it is "conducting a life on the fringe ", and is not widely applied, mainly due to the restricted applicability of many of the techniques. In this paper we propose a symmetry reduction technique applied to high-level formal specification languages (B and Z). Not only does symmetry arise naturally in most models, it can also be exploited without restriction by our method. This method translates states of a formal model into directed graphs, and then uses graph canonicalisation to detect symmetries. We use the tool NAUTY to efficiently perform graph canonicalisation, which we have interfaced with the model checker ProB. In this paper we present the general technique, show how states can be translated first into vertex-coloured graphs suitable for NAUTY. We present empirical results, showing the effectiveness of our method as well as analysing the cost of graph canonicalisation.

Symmetry reduction is a technique that can help alleviate the problem of state space explosion in model checking. The idea is to verify only a subset of states from each class (orbit) of symmetric states. This paper presents a framework for symmetry reduced model checking of B machines, which verifies a unique representative from each orbit. Symmetries are induced by the deferred set; a key component of the B language. This contrasts with strategies that require the introduction of a special data type into a language, to indicate symmetry. An extended version of the graph isomorphism program, nauty, is used to detect symmetries, and the symmetry reduction package has been integrated into the PROB model checker. Relevant algorithms are presented, and experimental results illustrate the effectiveness of the method, where exponential speedups are sometimes possible.

We present ECCE and LOGEN, two partial evaluators for Prolog using the online and offline approach respectively. We briefly present the foundations of these tools and discuss various applications. We also present new implementations of these tools, carried out in Ciao Prolog. In addition to a command-line interface new user-friendly web interfaces were developed. These enable non-expert users to specialise logic programs using a web browser, without the need for a local installation.

The paper develops a self-tuning resource aware partial evaluation technique for Prolog programs, which derives its own control strategies tuned for the underlying computer architecture and Prolog compiler using a genetic algorithm approach. The algorithm is based on mutating the annotations of offline partial evaluation. Using a set of representative sample queries it decides upon the fitness of annotations, controlling the trade-off between code explosion, speedup gained and specialisation time. The user can specify the importance of each of these factors in determining the quality of the produced code, tailoring the specialisation to the particular problem at hand. We present experimental results for our implemented technique on a series of benchmarks. The results are compared against the aggressive termination based binding-time analysis and optimised using different measures for the quality of code. We also show that our technique avoids some classical pitfalls of partial evaluation.

No abstract available.

We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access policy specification. We then proceed to specialise the meta-program for a given access policy and intensional database by using the logen partial evaluation system. In addition to describing the programs involved in our approach, we give a number of performance measures for our implementation of an access control checker, and we discuss the implications of using this approach for access control on deductive databases. In particular, we show that by using our approach we get flexible access control with virtually zero overhead.

Abstract Object Petri nets (OPNs) provide a natural and modular method for the modelling of many real-world systems. We give a structure-preserving translation of OPNs to Prolog, avoiding the need for an unfolding to a flat Petri net. The translation provides support for reference and value semantics, and even allows different objects to be treated as copyable or non-copyable, respectively. The method is developed for OPNs with arbitrary nesting. We then apply logic programming tools to animate, compile and model check OPNs. In particular, we use the partial evaluation system logen to produce an OPN compiler, and we use the model checker xtl to verify CTL formulas. We also use logen to produce special purpose model checkers. We present two case studies, along with experimental results. A comparison to OPN translations to Maude specifications and model checking is given, showing that our approach is roughly twice as fast for larger systems. We also tackle infinite state model checking using the ecce system.

Recently the relationship between abstract interpretation and program specialization has received a lot of scrutiny, and the need has been identified to extend program specialization techniques so as to make use of more refined abstract domains and operators. This article clarifies this relationship in the context of logic programming, by expressing program specialization in terms of abstract interpretation. Based on this, a novel specialization framework, along with generic correctness results for computed answers and finite failure under SLD-resolution, is developed.This framework can be used to extend existing logic program specialization methods, such as partial deduction and conjunctive partial deduction, to make use of more refined abstract domains. It is also shown how this opens up the way for new optimizations. Finally, as shown in the paper, the framework also enables one to prove correctness of new or existing specialization techniques in a simpler manner.The framework has already been applied in the literature to develop and prove correct specialization algorithms using regular types, which in turn have been applied to the verification of infinite state process algebras.

The so called “cogen approach” to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of both functional and imperative languages. This paper demonstrates that the cogen approach is also applicable to the specialisation of logic programs (called partial deduction) and leads to effective specialisers. Moreover, using good binding-time annotations, the speed-ups of the specialised programs are comparable to the speed-ups obtained with online specialisers. The paper first develops a generic approach to offline partial deduction and then a specific offline partial deduction method, leading to the offline system LIX for pure logic programs. While this is a usable specialiser by itself, it is used to develop the cogen system LOGEN. Given a program, a specification of what inputs will be static, and an annotation specifying which calls should be unfolded, LOGEN generates a specialised specialiser for the program at hand. Running this specialiser with particular values for the static inputs results in the specialised program. While this requires two steps instead of one, the efficiency of the specialisation process is improved in situations where the same program is specialised multiple times. The paper also presents and evaluates an automatic binding-time analysis that is able to derive the annotations. While the derived annotations are still suboptimal compared to hand-crafted ones, they enable non-expert users to use the LOGEN system in a fully automated way. Finally, LOGEN is extended so as to directly support a large part of Prolog's declarative and non-declarative features and so as to be able to perform so called mixline specialisations.

The past decade has seen dramatic growth in the application of model checking techniques to the validation and verification of correctness properties of hardware, and more recently software systems. Recently, there has been increasing interest in applying logic programming techniques to model checking in particular and verification in general. For example, table-based logic programming can be used as an efficient means of performing explicit model checking. Other research has successfully exploited set-based logic program analysis, constraint logic programming, and logic program transformation techniques to verify systems.

Program specialisation aims at improving the overall performance of programs by performing source to source transformations. A common approach within functional and logic programming, known respectively as partial evaluation and partial deduction, is to exploit partial knowledge about the input. It is achieved through a well-automated application of parts of the Burstall-Darlington unfold/fold transformation framework. The main challenge in developing systems is to design automatic control that ensures correctness, efficiency, and termination. This survey and tutorial presents the main developments in controlling partial deduction over the past 10 years and analyses their respective merits and shortcomings. It ends with an assessment of current achievements and sketches some remaining research challenges.

In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper focuses on one particular class of problem--coverability for (infinite state) Petri nets--and shows how existing techniques and tools for declarative programs can be successfully applied. In particular, we show that a restricted form of partial deduction is already powerful enough to decide all coverability properties of Petri Nets. We also prove that two particular instances of partial deduction exactly compute the Karp-Miller tree as well as Finkel's minimal coverability set. We thus establish an interesting link between algorithms for Petri nets and logic program specialisation.

Given a program and some input data, partial deduction computes a specialized program handling any remaining input more efficiently. However, controlling the process well is a rather difficult problem. In this article, we elaborate global control for partial deduction: for which atoms, among possibly infinitely many, should specialized relations be produced, meanwhile guaranteeing correctness as well as termination? Our work is based on two ingredients. First, we use the concept of a characteristic tree, encapsulating specialization behavior rather than syntactic structure, to guide generalization and polyvariance, and we show how this can be done in a correct and elegant way. Second, we structure combinations of atoms and associated characteristic trees in global trees registering “causal” relationships among such pairs. This allows us to spot looming nontermination and perform proper generalization in order to avert the danger, without having to impose a depth bound on characteristic trees. The practical relevance and benefits of the work are illustrated through extensive experiments. Finally, a similar approach may improve upon current (on-line) control strategies for program transformation in general such as (positive) supercompilation of functional programs. It also seems valuable in the context of abstract interpretation to handle infinite domains of infinite height with more precision.

In [23] we presented a partial evaluation scheme for a "real tomatically generating highly specialised update procedures for deductive databases.