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. 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. 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. 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. 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. 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. 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. 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.

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.