Model checking of software has been a very active research topic recently. As a result, a number of software model checkers have been developed for analysis of software written in ...
Abstract. Historically, dynamic techniques are the pioneers of the area of information flow in the 70's. In their seminal work, Denning and Denning suggest a static alternativ...
Abstract. The Java Supercompiler (JScp) is a specializer of Java programs based on the Turchin's supercompilation method and extended to support imperative and object-oriented...
A term t is called a template of terms t1 and t2 iff t1 = t1 and t2 = t2, for some substitutions 1 and 2. A template t of t1 and t2 is called the most specific iff for any template...
Peter E. Bulychev, Egor V. Kostylev, Vladimir A. Z...
Abstract. Searching in metric spaces is a very active field since it offers methods for indexing and searching by similarity in collections of unstructured data. These methods sele...
Abstract. We present an algorithm for generating all polynomial invariants of Psolvable loops with assignments and nested conditionals. We prove termination of our algorithm. The p...
Kohn’s Molecular Interaction Maps (MIMs) are a graphical notation for describing bioregulatory networks at the molecular level. Even if the meaning of Kohn’s diagrams can be of...
Roberto Barbuti, Daniela Lepri, Andrea Maggiolo-Sc...
Abstract. Data privacy is an important application of ontology modularization. The aim is to publish one module while keeping the information of another module private. We show how...
Abstract. The article concerns problems of formulating standard requirements to implementations of mathematical functions working with floating-point numbers and conformance test ...