Wyniki wyszukiwania - BazTech

1

Forward and backward static analysis for critical numerical accuracy in floating-point programs

Thushara M. G., Somasundaram K.

Computer Science

|

2020

|

T. 21 (2)

179--192

EN

In this article, we introduce a new static analysis for numerical accuracy. We address the problem of determining the minimal accuracy on the inputs and on the intermediary results of a program containing foating-point computations in order to ensure a desired accuracy on the outputs. The main approach is to combine a forward and a backward static analysis, done by abstract interpretation. The backward analysis computes the minimal accuracy needed for the inputs and intermediary results of the program in order to ensure a desired accuracy on the results, specied by the user. In practice, the information collected by our analysis may help to optimize the formats used to represent the values stored in the variables of the program or to select the appropriate sensors. To illustrate our analysis, we have shown a prototype example with experimental results.

2

Observational Completeness on Abstract Interpretation

Amato G., Scozzari F.

Fundamenta Informaticae

|

2011

|

Vol. 106, nr 2-4

149-173

EN

In the theory of abstract interpretation, a domain is complete when abstract computations are as precise as concrete computations. In addition to the standard notion of completeness, we introduce the concept of observational completeness. A domain is observationally complete for an observable when abstract computations are as precise as concrete computations, if we only look at properties in . We prove that continuity of state-transition functions ensures the existence of the least observationally complete domain and we provide a constructive characterization. We study the relationship between the least observationally complete domain and the complete shell. We provide sufficient conditions under which they coincide, and show several examples where they differ, included a detailed analysis of cellular automata.

3

Verification of Concurrent Systems with Parametric Delays Using Octahedra

Clarisó R., Cortadella J.

Fundamenta Informaticae

|

2007

|

Vol. 78, nr 1

1-33

EN

A technique for the verification of concurrent parametric timed systems is presented. In the systems under study, each action has a bounded delay where the bounds are either constants or parameters. Given a safety property, the analysis computes automatically a set of constraints on the parameters that is sufficient to guarantee the property. The main contribution is an innovative representation of the parametric timed state space based on bit-vectors. Experimental results from the domain of timed circuits show that this representation improves the efficiency of the verification significantly with a small impact on the accuracy of the derived constraints.

4

Abstract Interpretation and Model Checking for Checking Secure Information Flow in Concurrent Systems

De Francesco N., Santone A., Tesei L.

Fundamenta Informaticae

|

2003

|

Vol. 54, nr 2,3

195-211

EN

We propose a method to check secure information flow in concurrent programs with synchronization. The method is based on the combination of abstract interpretation and model checking: by abstract interpretation we build a finite representation (transition system) of the behavior of the program. Then we model check the the abstract transition system with respect to the security properties, expressed by a set of temporal logic formulae. The approach allows certifying more programs than previous methods do. The main point is that we are able to check more carefully the scope of indirect information flows.