{'fraction_non_alphanumeric': 0.02052117263843648, 'fraction_numerical': 0.0, 'mean_word_length': 5.384615384615385, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Infinite State Model Checking using Partial Evaluation and Abstract Interpretation

Logic programming originated from the discovery that a subset of predicate logic could be given a procedural interpretation which was first embodied in the programming language Prolog. The unique features of logic programming make it appealing for numerous applications in artificial intelligence, computer-aided verification, etc. Program specialisation, also called partial evaluation, is an automatic tool for program optimisation, similar in concept to, but in several ways stronger than highly optimising compilers. The central idea is to specialise a given source program for a particular application domain. Program analysis is about statically inferring information about dynamic program properties. Abstract interpretation was developed as a very general, formal framework for specifying and validating program analyses. The past years have seen dramatic growth in the application of model checking techniques to the validation and verification of hardware systems. The main idea is to model a hardware or software system as a finite, labeled transition system (LTS) which is then exhaustively explored to decide whether a given specification holds for all reachable states. Recently there has been interest in applying logic programming techniques to model checking. E.g., table-based logic programming can be used as an efficient means of performing explicit model checking. Furthermore, logic programming provides a good basis to formulate many other specification formalisms (a claim which we have further investigated in this project). However, despite the success of model checking, most systems must be substantially simplified (i.e., abstracted) before they can be model checked and substantial human intervention is usually required for this process. Furthermore, most software systems cannot be modeled directly by a finite state system. For these reasons, there has recently been considerable interest in infinite model checking. This, by its very undecidable nature, is a daunting task, for which abstraction is a key issue as it may allow one to approximate an infinite system by a finite one. Overall Goal This research aims at exploring automatic means of building precise but tractable abstractions for infinite model checking (or model checking of finite, but very complex systems). We propose to do this by extending technology that has been developed to tackle similar problems in the context of automatic logic program analysis and specialisation. Indeed, a major concern of partial evaluation is the automation of control and abstraction, and, in the current state-of-the-art, this has obtained a level of refinement which goes beyond mere heuristic strategies. We will study to what extent we can leverage this technology for infinite model checking. Finally, it is often felt that there is a close relationship between abstract interpretation and program specialisation and, recently, there has been a lot of interest in integrating these two techniques.