An approach to visualization of knowledge portal content

The process of development of an ontology-based knowledge portal and creation of its content is time-consuming and labor-intensive. It is very desirable to have special analysis facilities for maintenance and development of such a portal. The subject of our paper is a tool for visual analysis of content and ontology...

apanovih.pdf880.43 KB

The uniform constraint solving API for UniCalc

The paper describes a programming interface that we have developed to separate constraints, solvers, and cooperation strategies in a constraint programming toolkit UniCalc. The interface is simple but it allows us to express such constraint solving techniques as increasing the level of consistency, various strategies for exhaustive search, and cooperation...

petrov.pdf103.12 KB

The problems of C program verification

The fully automatic verification of programs is a tempting and hardly accessible goal of modern programming. The low-level nature of the most popular programming languages, such as C and C+, has raised its difficulty to a new level. New formal methods and specification languages are required, because the classical Hoare...

promsky.pdf165.46 KB

The language of calculus of computable predicates as a minimal kernel for functional languages

Logical semantics is a new kind of formal semantics used to describe semantics of pure call-by-value functional languages. For the statement S, the logical semantics LS(S) is a predicate that is true for the variable values for which the execution of S is finished. Let a specification of the statement...

shelekhov.pdf124.66 KB

Fabulous arrays I: Operational and transformational semantics of static arrays in verification project F@BOOL@

The purpose of the F@BOOL@ project is to develop a transparent for users, compact, portable and extensible verifying compiler F@BOOL@ for annotated computer programs, that uses effective and sound automatic programs for checking satisfiability of propositional Boolean formulas. The kernel programming language of the project interprets all variables by residuals...

shilov.pdf202.18 KB