Sistemas de Tipos para Verificación de Programas Concurrentes. Type Systems for Concurrent Programs Verification.

La programación concurrente es una tarea difícil aún para los más experimentados programadores. Las investigaciones en concurrencia han dado como resultado una gran cantidad de mecanismos y herramientas para resolver problemas de condiciones de carrera de datos y deadlocks, problemas que surgen por el mal uso de los mecanismos de sincronización. La verificación de propiedades interesantes de programas concurrentes presenta dificultades extras a los programas secuenciales debido al no-determinismo de su ejecución, lo cual resulta en una explosión en el número de posibles estados de programa, haciendo casi imposible un tratamiento manual o aún con la ayuda de computadoras. Algunos enfoques se basan en la creación de lenguajes de programación con construcciones con un alto nivel de abstración para expresar concurrencia y sincronización. Otros enfoques tratan de desarrollar técnicas y métodos de razonamiento para demostrar propiedades, algunos usan demostradores de teoremas generales, model-checking o algortimos específicos sobre un determinado sistema de tipos. Los enfoques basados en análisis estático liviano utilizan técnicas como interpretación abstracta para detectar ciertos tipos de errores, de una manera conservativa. Estas técnicas generalmente escalan lo suficiente para aplicarse en grandes proyectos de software pero los tipos de errores que pueden detectar es limitada. Algunas propiedades interesantes están relacionadas a condiciones de carrera y deadlocks, mientras que otros están interesados en problemas relacionados con la seguridad de los sistemas, como confidencialidad e integridad de datos. Los principales objetivos de esta propuesta es identificar algunas propiedades de interés a verificar en sistemas concurrentes y desarrollar técnicas y herramientas para realizar la verificación en forma automática. Para lograr estos objetivos, se pondrá énfasis en el estudio y desarrollo de sistemas de tipos como tipos dependientes, sistema de tipos y efectos, y tipos de efectos sensibles al flujo de datos y control. Estos sistemas de tipos se aplicarán a algunos modelos de programación concurrente como por ejemplo, en Simple Concurrent Object-Oriented Programming (SCOOP) y Java. Además se abordarán propiedades de seguridad usando sistemas de tipos específicos. Concurrent programming has remained a dificult task even for very experienced programmers. Concurrency research has provided a rich set of tools and mechanisms for dealing with data races and deadlocks that arise of incorrect use of synchronization. Verification of most interesting properties of concurrent programs is a very dificult task due to intrinsic non-deterministic nature of concurrency, resulting in a state explosion which make it almost imposible to be manually treat and it is a serious challenge to do that even with help of computers. Some approaches attempts create programming languages with higher levels of abstraction for expressing concurrency and synchronization. Other approaches try to develop reasoning methods to prove properties, either using general theorem provers, model-checking or specific algorithms on some type systems. The light-weight static analysis approach apply techniques like abstract interpretation to find certain kind of bugs in a conservative way. This techniques scale well to be applied in large software projects but the kind of bugs they may find are limited. Some interesting properties are related to data races and deadlocks, while others are interested in some security problems like confidentiality and integrity of data. The main goals of this proposal is to identify some interesting properties to verify in concurrent systems and develop techniques and tools to do full automatic verification. The main approach will be the application of type systems, as dependent types, type and effect systems, and flow-efect types. Those type systems will be applied to some models for concurrent programming as Simple Concurrent Object-Oriented Programming (SCOOP) and Java. Other goals include the analysis of security properties also using specific type systems.

El valor razonable como concepto vinculado a la pertinencia del valor. Fair value as a concept related to value relevance.

IDENTIFICACIÓN Y CARACTERIZACIÓN DEL PROBLEMA - HIPÓTESIS Según la NIC 39, el valor razonable es la cantidad por la que puede ser intercambiado un activo o cancelado un pasivo entre un comprador y un vendedor interesados y debidamente informados, en condiciones de independencia mutua. La definición del FASB (SFAC 7) es muy similar, y define el valor razonable como el monto mediante el que un activo podría ser enajenado en una transacción entre partes independientes, dispuestas a realizar la operación en situaciones diferentes a la de una liquidación o a la de una venta forzada. Puede apreciarse que esta definición de valor razonable es limitada porque, a excepción de escenarios que se correspondan con mercados perfectos y completos, el concepto puede abarcar valores de entrada, valores de salida y valores en uso, los cuales pueden ser muy diferentes (Beaver, 1987). El valor de entrada es el valor de adquisición o de reemplazo, el valor de salida es el precio al cual un activo puede ser vendido o liquidado, y el valor en uso es el valor incremental de una empresa atribuible a un activo (se correspondería con el valor presente mencionado anteriormente). Dado que el IASB y la FASB se ocupan de la valuación de activos que una empresa posee, y no de activos que serán adquiridos en un futuro, su definición de valor razonable debería ser interpretada desde la perspectiva del vendedor. Por lo tanto, el concepto de valor razonable que manejan el IASB y la FASB se asemeja a un valor de salida, tal como lo propusieron Chambers y Stirling hace bastantes años atrás.Planteado esto, lo que tratará de dilucidar este proyecto de investigación es si este concepto de valor razonable es realmente novedoso o es una simple regresión a los valores corrientes de salida defendidos por los autores de la década del setenta. OBJETIVOS GENERALES Y ESPECÍFICOS General Analizar si el concepto “valor razonable” tal como es definido por la normativa actual se corresponde con una definición novedosa o es una adaptación/modificación/regresión de conceptos ya existentes (valores corrientes de salida). Específicos Revisar la literatura específica desde el punto de vista de la teoría contable y las normas de las que dispone la profesión referidas a los siguientes aspectos: a) Valores corrientes b) Valor razonable MATERIALES Y MÉTODOS El análisis que se llevará a cabo comprenderá dos aspectos. El primero consiste en la revisión de la doctrina contable. Para ello se analizará bibliografía significativa y trabajos de eventos académicos relacionados con el valor razonable. En segundo término se revisará la normativa profesional a nivel nacional e internacional. Después de concluido con los pasos anteriores se analizará la novedad del concepto valor razonable y su semejanza con el valor corriente de salida planteado por los autores de la década del setenta. IMPORTANCIA DEL PROYECTO – IMPACTO Se pretende revisar si el concepto valor razonable planteado por la normativa actual resulta realmente novedoso o es una adaptación de viejos conceptos planteados en la década del setenta del siglo pasado. El proyecto resulta importante porque es un tema no desarrollado en la literatura, ni planteado en congresos. Se estima lograr material de publicación y presentación en eventos académicos. According to the NIC 39, fair value is the quantity for the one that can be exchanged an asset or cancelled a liability between a buyer and a seller interested and due informed, in conditions of mutual independence. The definition of the FASB (SFAC 7) is very similar, and defines fair value as the amount by means of which an assets might be alienated in a transaction between independent parts, ready to realize the operation in situations different from that of a liquidation or to that of a forced sale. This definition of reasonable value is limited because, with the exception of scenes that fit with perfect and complete markets, the concept can include values of entry, values of exit and values in use, which can be very different (Beaver, 1987). The value of entry is the value of acquisition or of replacement, the value of exit is the price to which an asset can be sold or liquidated, and the value in use is the incremental value of a company attributable to an asset. Provided that the IASB and the FASB deal with the appraisal of assets that a company possesses, and not of assets that will be acquired in a future, this definition of fair value should be interpreted from the perspective of the seller. Therefore, the concept of reasonable value that they handle the IASB and the FASB is alike a value of exit, as Chambers and Stirling proposed it enough years ago behind. We will review if the concept of "fair value" is really new or if it is an adaptation of old concepts.