PAS 2014 PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. In this talk I will give an overview on the main ideas of my "Theorema" approach to mathematics, which reflects my view on mathematics that evolved over my life as a mathematician ("from 17 to 71"):

- Mathematics is the "art of explanation", the art of reducing the complex to the simple. Hence, mathematics is of highest relevance for the "wo-man on the street".

- Mathematics is in the center of the "innovation spiral" that starts from basic research on the nature of nature and goes all the way via technology to economy and welfare. Hence, mathematics is of highest relevance to our society.

- Mathematics is the meta-theory of itself. It can explain how we derive new mathematical knowledge and methods from available knowledge and methods. This is possible because mathematics is essentially formal. The application of mathematics to itself, i.e. to the mathematical exploration process, was hardly noticeable until the middle of 20th century. However, now, we can observe what "application of mathematics to itself" means practically. This will be of highest relevance to the way we will do mathematics (including software) in the future, i.e. the (semi-)automation of the mathematical exploration process will be of highest relevance to the "working mathematicians".

I think that predicate logic (in some nicely readable two-dimensional - even user-definable - syntax) is the natural frame for providing a version of mathematics that pleases the wo-man from the street, society, and the working mathematicians. And all the effort and attention must go to automating natural reasoning in predicate logic for pleasing everybody with more and more attractive mathematics.

This is the reason why approximately in the middle of the 1990-ies I launched the Theorema Project.

In the talk, I will give an overview on the current state of the project, which - due to my many services for "society" that took lots of my time - is not yet at a stage which is satisfactory. However, I hope I will be able to explain a few highlights and to draw a picture from which the avenues to the future can be guessed.

Of course, Theorema is just one in a group of research projects that pursue the automation of mathematics. I am very optimistic, nervous, and excited to enjoy the dawn of a new era of mathematics that will put mathematics right into the center of modern society in a tangible, natural, artistic and surprising way.

ABSTRACT. Cryptographic protocols such as IKE, SET, TLS, Kerberos have been developed to secure electronic transactions. However the design of such protocols often appears to be problematic even assuming that the cryptographic primitives are perfect, i.e. even assuming we cannot decrypt a message without the proper key. An intruder may intercept messages, analyse them, modify them without much ressources and then carry out malevolent actions. This may lead to a variety of attacks such as well-known Man-In-The-Middle attacks. In this setting, the so-called Dolev-Yao model, protocol analysis can be automated by designing suitable symbolic constraint solving techniques. Messages are represented by terms and intruder actions are simulated by deduction rules. It is also possible to somewhat relax the perfect encryption hypothesis by taking into account some algebraic properties of operators. Secrecy and authentification properties, as expected of correct protocol specifications, are verified by showing that no sequence of intruder actions leads to a failure state.

We present some applications of the same security protocol analysis techniques to service oriented computing such as the synthesis of a secure composed service and its validation. In this original framework intruder actions are replaced by mediator actions and the failure states are replaced by accepting states for both client and services.

ABSTRACT. The pattern calculus described in this paper integrates the functional mechanism of the lambda-calculus with the capabilities of finitary pattern matching algorithms. We propose a generic confluence proof, where the way pattern abstractions are applied in a non-deterministic calculus is axiomatized. Instances of the matching function are presented.

ABSTRACT. R-calculus is an inference system to formally deduce all possible maximal contractions of a theory in first-order language. Based on the theories of R-calculus, we implemented a software toolkit, called RCK, to perform R-calculus on computer. The toolkit enable users to obtain and verify maximal contractions of a given theory whenever the theory is refuted by given facts. We briefly introduce the framework of RCK and demonstrate how R-calculus can serve for scientific discovery.

ABSTRACT. We show that, given the operational semantics of two programming languages L and R, it is possible to construct an aggregate language, in which programs consist of pairs of programs from L and respectively R. In the aggregate language, a program P = (PL, PR) takes a step from either PL or PR. The main difficulty is how to aggregate the two languages so that data such as integers or booleans that are common to both languages has the same representation in the aggregate language. The aggregation is based on the pushout theorem, which allows us to construct a model of the aggregate language from models of the initial languages, while making sure that the interpretation of common data such as integers is the same. The main application of the aggregation result is in equivalence checking. It is possible to check for example that two programs PL and PR (written in L and respectively R) compute the same result by checking the partial correctness of the pair (PL,PR) in the aggregate language.

ABSTRACT. We choose to represent sets as sorted lists without duplications, which we call monotone lists. Without loss of generality, we assume that the elements of the sets are from an ordered domain, and we take increasingly sorted lists. This approach leads to more ecient algorithms then the ones for operating on sets represented as non-sorted lists. We use two functions: the function R which applied to a set returns its representation as a monotone list, and the function S which applied to a (monotone) list returns its corresponding set. These two functions are bijective and reverse to each other and represent the isomorphism between the domain of nite sets (with the usual signature) and the domain of monotone lists with the appropriate signature induced by this isomorphism. The synthesis problem consists in producing the algorithms implementing this signature.

Each synthesis starts as an inductive constructive proof which applies specic strategies and inference rules. These strategies and inference rules are based on the corresponding properties of sets (as monotone lists). We synthesize (by extracting from proofs) ve algorithms among with two predicates: Member and Inclusion; and three functions: Union, Intersection, and Difference.

In parallel with the process of algorithm synthesis we explore the theory of monotone lists.

ABSTRACT. Constraint solving is one of the essential parts of symbolic execution. Most of the constraint solvers are aimed at a particular kind of constraint and might have no way to deal with complex path constraints derived from real-world applications. To tackle the problem, we propose a hybrid solving strategy for path constraints containing multiple kinds of constraints. In particular, a split approach is used to cut the whole path constraint into several parts that can be solved by different constraint solving techniques. Next, the local method of meta-heuristic search is used to solve non-linear constraints led by the solutions produced by a linear constraint solver. We have extended the constraint solver in the symbolic execution engine KLEE-FP with our approach and evaluated its effectiveness on a set of mathematical programs. The results show that our approach can solve a majority of complex path constraints in reasonable time.

ABSTRACT. Operating system is a huge software with complicated functionality. The correctness of even single module cannot be proved through software test. Project seL4 has proved the correctness of each function of a microkernel operating system. The correctness of each single function of an operating system cannot prove its integrity and other security property. In this paper we proposed a OS model of finite state machine (OSMFSM). We design our VTOS(Verified Trusted Operating System), which is a microkernel operating system and aimed at being formally verified and trusted, according to this model. We define the state of the OSMFSM through the global objects in VTOS, and the transition function of the OSMFSM as a piecewise defined function through the functions in VTOS. Through establishing a domain for VTOS with the help of OSMFSM and another domain, which is isomorphic to the former, in Isabelle/HOL, we prove the correctness of some functions in the microkernel of VTOS formally. With the help of the concept of the invariability of the FSM, we propose a method of describing and proving the integrity of an OS.

ABSTRACT. This paper presents three verified conversion algorithms between finite automata in Isabelle/HOL. The specifications of all algorithms are formalized in a direct way, from which Isabelle/HOL can generate executable programs. The correctness of each algorithm is totally verified from three perspectives: the loops in each algorithm terminate, the output of an algorithm is an automata with the expected type, and the input and output of one conversion algorithm accept the same language. The whole work includes over 3000 lines of code in Isabelle/HOL.

ABSTRACT. Symbolic analysis is known and valued for its strength of statically inferring non-trivial properties of programs. This strength, however, comes typically at high computation costs often preventing a full path coverage of programs of real-world applications.

In this presentation we reconsider and highlight two examples of successfully coping and circumventing the scalabality issue related to straightforward applications of symbolic analysis in the timing analysis of real-time systems. In the first approach, we restrict symbolic analysis to program loops matching particular structural patterns for which symbolic analysis reduces to the solution of a set of recurrence equations which does not require an explicit symbolic path analysis and coverage of these loops. In the second approach, we focus the pathwise symbolic analysis of a program to a set of program paths which are known by other program analyses to be crucial for the timing behaviour of the program that is usually small and manageable. Both approaches have important complementary orthogonal applications in different stages of the timing analysis of safety-critical real-time systems and proved to be useful in practice.

ABSTRACT. The paper presents new predicate transformer for symbolic modeling. Predicate transformer is a symbolic function that is used for computing transitions of a system with states represented by means of first-order formulas. Systems under consideration are compositions of environments and agents inserted into these environments (insertion models). They are specified by means of basic protocols, which represent formal requirements to systems. Previous version of predicate transformer allowed only existential quantifiers in formulas. A new one allows both quantifiers but with some restriction on formulas. The use of universal quantifier is illustrated on the example of MESI protocol.

ABSTRACT. In 1935, Karl Popper published his famous book entitled ``The Logic of Scientific Discovery.'' In this book he proposed a general procedure of scientific discovery which contains the following key points. (1) A scientific theory consists of ``conjectures'' about domain knowledge.(2) Every conjecture may be disproved, that is, conclusions or predictions derived on the basis of it may be and must be subject to verification using the results of observations of human beings and scientific experiments on natural phenomena. (3) When the conclusions or predications contradict the results of observations or experiments, the theory is refuted by facts. (4) In this case, one should abandon those conjectures in the current theory which lead to contradictions, propose new conjectures, and form a new theory. (5) Every theory obtained in this way is provisional: it is expected to be refuted by facts any time. Truth in science is reached in the process of unlimited explorations.

The above procedure is given in the layer of Scientific Philosophy. In this paper, we provide a mathematical-logical framework for this general procedure. It consists of the following four parts. (1) Representability theory, that is, the theory of representing basic concepts such as theory, conjecture, provability, and refutation by facts, which are involved in the general procedure of scientific discovery, in first-order languages. (2) R-calculus, that is, a revision calculus for deleting conjectures refuted by facts or experiments from the current theory. It is a formal inference system about logical connective symbols and quantifier symbols and is sound, complete, and reachable. (3) Theory of version evolution, that is, the theory about version sequences, their limits, proschemes, and the convergency, soundness, and independency of proschemes. (4) I-calculus, that is, a calculus for forming conjectures. It is a formal inference system about contexts and involves the theory of rationality about conjecture calculus.

The above four parts constitute the mathematical framework for the logic of scientific discovery, which may be viewed as a formal description of ``the logic of scientific discovery.'' As examples, we will use this mathematical framework to give formal descriptions of the processes of Einstein's discovery of ``the special theory of relativity" and Darwin's proposal of ``the theory of evolution.'' The difference between our mathematical framework and the general procedure of Popper's logic of scientific discovery in the sense of scientific philosophy is: the former can be implemented on computer, so that the revision of scientific theories and evolution of version sequences can be accomplished via human-computer interactions and in the case where the current theory encounters refutation by facts, the computer can provide schemes for rational revision.

ABSTRACT. We describe work in progress on constructing a complete implementation of Weispfenning's virtual term substitution method for real closed field formulas of unbounded degree. We build upon a recent high-performance library for computing over non-Archimedean real closed fields using Thom's Lemma.

(Extended abstract)

ABSTRACT. In this paper, we propose a model theory for R-calculus without cut. First, validity of R-transitions and R-transition sequences is defined using models of first-order languages. Then reducibility of R-transition sequences is defined and it is proved that every R-transition sequence, which transits to an R-termination, can be reduced to an irreducible R-transition sequence. Finally, the soundness and completeness of R-calculus is redefined. And R-calculus without cut is proved to still be sound and complete.

ABSTRACT. Programs are typically written by humans and executed by computers in order to solve problems over a specific domain. A program - a sequence of instructions executable by a computer - represents the encoded algorithm for solving the problem. The algorithm and data structures are created by the mental understanding of the problem given. This representation also addresses details such as run time efficiency, understandability, or maintainability.

Conversely when a programmer tries to understand a program he/she decodes the program again into an abstract mental model. From this model the programmer can start to improve or change the program, which is again encoded and represented as a modified program.

In this paper we show a problem solving process that starts with finding, enhancing or inventing a logical theory over first order predicate logic. This theory represents the concepts of the problem domain, relations between the concepts, and operations. A theory is a set of formulae. Operations on terms of the theory correspond to functionality of the solution. These operations can be characterized by partial functions from given input to expected output. Requirements formally express the functionality of the operations and are commonly defined using input/output conditions. If an operation's input satisfies the input condition then operation's output (if obtainable) satisfies the output condition.

The process is incremental. It is important to capture the high level requirements. For representing the solution as a machine executable program, the theory should be sufficiently refined so that the requirements satisfy the problem and capture important properties of the execution environment. Detailed conditions make it possible to formally evaluate different design approaches. Design approach refers to the abstractions and methods used for framing the algorithms. As an example in the hash table design it is important to capture the concept of collisions in the table abstractly in order to compare different strategies how to handle collisions.

ABSTRACT. Research and industrial experience reveal that code reviews as a part of software inspection might be the most cost-effective technique a team can use to reduce defects. Tools that automate code inspection mostly focus on the detection of a priori known defect patterns and security vulnerabilities. Automated detection of logical errors, due to a faulty implementation of applications’ functionality is a relatively uncharted territory. Automation can be based on profiling the intended behavior behind the source code. In this paper, we present a code profiling method based on token classification. Our method combines an information flow analysis, the crosschecking of dynamic invariants with symbolic execution and code classification heuristics with the use of a fuzzy logic system. Our goal is to detect logical errors and exploitable vulnerabilities. The theoretical underpinnings and the practical implementation of our approach are discussed. We test the APP_LogGIC tool that implements the proposed analysis on two real-world applications. The results show that profiling the intended program behavior is feasible in diverse applications. We discuss in detail the heuristics used to overcome the problem of state space explosion and that of the large data sets. Code metrics and test results are provided to demonstrate the effectiveness of the proposed approach. This paper extends the work reported in an article that has been recently submitted to an international conference and is currently pending review. In this extended version of our method we propose new classification mechanisms and we provide a detailed description of the used source code classification techniques and heuristics.

ABSTRACT. In the setting of classical first-order logic with inductive predicates, two kinds of sequent-based induction reasoning are distinguished: cyclic and structural. Proving their equivalence is of great theoretical and practical interest for the automated reasoning community. It has been shown previously how to transform structural proofs developed with the LKID system into cyclic proofs using the CLKID$^\omega$ system. However, the inverse transformation was only conjectured.

We provide a simple procedure that performs the inverse transformation for an extension of LKID with explicit induction rules issued from the structural analysis of CLKID$^{\omega}$ proofs, then establish the equivalence of the two systems. This result is further refined for an extension of LKID with Noetherian induction rules. Based on it, we propose a solution for validating cyclic reasoning by (higher-order) sequent-based systems integrating the Noetherian induction principle, like Coq.

ABSTRACT. We present an automatic testing tool for Android apps. The tool accepts specifications in an extension of LTL (Linear Temporal Logic) and then automatically crawls the screen activities. We report experiments with the random test plan.