## Unified semantic language: syntax, semantics, and pragmatics

A new language of finite state machines called USL is proposed. The language is intended for rapid development of formal verification-oriented operational semantics of modern programming languages. Formal operational semantics of the USL language is defined. The USL-based approach to programming language semantics design is illustrated by the example of...

## Timed testing for dense timed model

In this paper, we try to decide a problem of recognising timed testing equivalences for timed event structures with dense internal actions. For this purpose, we construct a formula that characterizes a timed event structure up to the timed *must*-preorder. So, to understand if two timed event structures are...

## Model checking μ-calculus in well-structured transition systems

We study the model checking problem for fixpoint logics in well- structured multiaction transition systems. P.A. Abdulla et al. (1996) and Finkel & Schnoebelen (2001) examined the decidability problem for liveness (reachability) and progress (eventuality) properties in well-structured single action transition systems. Our main result is as follows: the model...

## A three-level approach to C# program verification

A new three-level approach to sequential object-oriented program verification is presented. It is applied to a significant С# subset called C#-light that includes all principal sequential С# constructs. At the first stage, C#-light is translated into an intermediate language C#-kernel that allows us to simplify axiomatic semantics. At the second...

## Integrated enterprise-level security solution “Vostok”

This work considers a model of a multilevel information system that integrates heterogeneous classes of objects of different configuration and complexity range. The architectural solution is suggested that allows dynamical extension of a working system by connecting objects both of existing classes and new classes as well. The use of...

## Logical characterization of probabilistic τ-bisimulation equivalences

Stochastic Petri nets (SPNs) is a well-known model for quantitative analysis. We consider the class called DTWSPNs that is a modification of discrete time SPNs (DTSPNs) by transition labeling and weights. Transitions of DTWSPNs are labeled by actions that represent elementary activities and can be visible or invisible for an...

## Algebraic semantics of an imperative programming language as a compiler abstract model

It is shown in the paper that state-based algebraic semantics of an imperative program can be regarded as a compiler abstract model and can serve as a good assistant of the compiler designer.