-
Inductive Predicate Synthesis Modulo Programs (Extended)
Authors:
Scott Wesley,
Maria Christakis,
Jorge A. Navas,
Richard Trefler,
Valentin Wüstholz,
Arie Gurfinkel
Abstract:
A growing trend in program analysis is to encode verification conditions within the language of the input program. This simplifies the design of analysis tools by utilizing off-the-shelf verifiers, but makes communication with the underlying solver more challenging. Essentially, the analyzer operates at the level of input programs, whereas the solver operates at the level of problem encodings. To…
▽ More
A growing trend in program analysis is to encode verification conditions within the language of the input program. This simplifies the design of analysis tools by utilizing off-the-shelf verifiers, but makes communication with the underlying solver more challenging. Essentially, the analyzer operates at the level of input programs, whereas the solver operates at the level of problem encodings. To bridge this gap, the verifier must pass along proof-rules from the analyzer to the solver. For example, an analyzer for concurrent programs built on an inductive program verifier might need to declare Owicki-Gries style proof-rules for the underlying solver. Each such proof-rule further specifies how a program should be verified, meaning that the problem of passing proof-rules is a form of invariant synthesis.
Similarly, many program analysis tasks reduce to the synthesis of pure, loop-free Boolean functions (i.e., predicates), relative to a program. From this observation, we propose Inductive Predicate Synthesis Modulo Programs (IPS-MP) which extends high-level languages with minimal synthesis features to guide analysis. In IPS-MP, unknown predicates appear under assume and assert statements, acting as specifications modulo the program semantics. Existing synthesis solvers are inefficient at IPS-MP as they target more general problems. In this paper, we show that IPS-MP admits an efficient solution in the Boolean case, despite being generally undecidable. Moreover, we show that IPS-MP reduces to the satisfiability of constrained Horn clauses, which is less general than existing synthesis problems, yet expressive enough to encode verification tasks. We provide reductions from challenging verification tasks -- such as parameterized model checking -- to IPS-MP. We realize these reductions with an efficient IPS-MP-solver based on SeaHorn, and describe a application to smart-contract verification.
△ Less
Submitted 11 July, 2024;
originally announced July 2024.
-
Quantum Network Tomography
Authors:
Matheus Guedes de Andrade,
Jake Navas,
Saikat Guha,
Inès Montaño,
Michael Raymer,
Brian Smith,
Don Towsley
Abstract:
Errors are the fundamental barrier to the development of quantum systems. Quantum networks are complex systems formed by the interconnection of multiple components and suffer from error accumulation. Characterizing errors introduced by quantum network components becomes a fundamental task to overcome their depleting effects in quantum communication. Quantum Network Tomography (QNT) addresses end-t…
▽ More
Errors are the fundamental barrier to the development of quantum systems. Quantum networks are complex systems formed by the interconnection of multiple components and suffer from error accumulation. Characterizing errors introduced by quantum network components becomes a fundamental task to overcome their depleting effects in quantum communication. Quantum Network Tomography (QNT) addresses end-to-end characterization of link errors in quantum networks. It is a tool for building error-aware applications, network management, and system validation. We provide an overview of QNT and its initial results for characterizing quantum star networks. We apply a previously defined QNT protocol for estimating bit-flip channels to estimate depolarizing channels. We analyze the performance of our estimators numerically by assessing the Quantum Cramèr-Rao Bound (QCRB) and the Mean Square Error (MSE) in the finite sample regime. Finally, we provide a discussion on current challenges in the field of QNT and elicit exciting research directions for future investigation.
△ Less
Submitted 18 May, 2024;
originally announced May 2024.
-
On the Characterization of Quantum Flip Stars with Quantum Network Tomography
Authors:
Matheus Guedes de Andrade,
Jake Navas,
Inès Montaño,
Don Towsley
Abstract:
The experimental realization of quantum information systems will be difficult due to how sensitive quantum information is to noise. Overcoming this sensitivity is central to designing quantum networks capable of transmitting quantum information reliably over large distances. Moreover, the ability to characterize communication noise in quantum networks is crucial in develo** network protocols cap…
▽ More
The experimental realization of quantum information systems will be difficult due to how sensitive quantum information is to noise. Overcoming this sensitivity is central to designing quantum networks capable of transmitting quantum information reliably over large distances. Moreover, the ability to characterize communication noise in quantum networks is crucial in develo** network protocols capable of overcoming the effects of noise in quantum networks. In this context, quantum network tomography refers to the characterization of channel noise in a quantum network through end-to-end measurements. In this work, we propose network tomography protocols for quantum star networks formed by quantum channels characterized by a single, non-trivial Pauli operator. Our results further the end-to-end characterization of quantum bit-flip star networks by introducing tomography protocols where state distribution and measurements are designed separately. We build upon previously proposed quantum network tomography protocols, as well as provide novel methods for the unique characterization of bit-flip probabilities in stars. We introduce a theoretical benchmark based on the Quantum Fisher Information matrix to compare the efficiency of quantum network protocols. We apply our techniques to the protocols proposed, and provide an initial analysis on the potential benefits of entanglement for Quantum Network Tomography. Furthermore, we simulate the proposed protocols using NetSquid to assess the convergence properties of the estimators obtained for particular parameter regimes. Our findings show that the efficiency of protocols depend on parameter values and motivate the search for adaptive quantum network tomography protocols.
△ Less
Submitted 11 July, 2023;
originally announced July 2023.
-
Quantum Network Tomography with Multi-party State Distribution
Authors:
Matheus Guedes de Andrade,
Jaime Días,
Jake Navas,
Saikat Guha,
Inès Montaño,
Brian Smith,
Michael Raymer,
Don Towsley
Abstract:
The fragile nature of quantum information makes it practically impossible to completely isolate a quantum state from noise under quantum channel transmissions. Quantum networks are complex systems formed by the interconnection of quantum processing devices through quantum channels. In this context, characterizing how channels introduce noise in transmitted quantum states is of paramount importance…
▽ More
The fragile nature of quantum information makes it practically impossible to completely isolate a quantum state from noise under quantum channel transmissions. Quantum networks are complex systems formed by the interconnection of quantum processing devices through quantum channels. In this context, characterizing how channels introduce noise in transmitted quantum states is of paramount importance. Precise descriptions of the error distributions introduced by non-unitary quantum channels can inform quantum error correction protocols to tailor operations for the particular error model. In addition, characterizing such errors by monitoring the network with end-to-end measurements enables end-nodes to infer the status of network links. In this work, we address the end-to-end characterization of quantum channels in a quantum network by introducing the problem of Quantum Network Tomography. The solution for this problem is an estimator for the probabilities that define a Kraus decomposition for all quantum channels in the network, using measurements performed exclusively in the end-nodes. We study this problem in detail for the case of arbitrary star quantum networks with quantum channels described by a single Pauli operator, like bit-flip quantum channels. We provide solutions for such networks with polynomial sample complexity. Our solutions provide evidence that pre-shared entanglement brings advantages for estimation in terms of the identifiability of parameters.
△ Less
Submitted 6 June, 2022;
originally announced June 2022.
-
DesCert: Design for Certification
Authors:
Natarajan Shankar,
Devesh Bhatt,
Michael Ernst,
Minyoung Kim,
Srivatsan Varadarajan,
Suzanne Millstein,
Jorge Navas,
Jason Biatek,
Huascar Sanchez,
Anitha Murugesan,
Hao Ren
Abstract:
The goal of the DARPA Automated Rapid Certification Of Software (ARCOS) program is to "automate the evaluation of software assurance evidence to enable certifiers to determine rapidly that system risk is acceptable." As part of this program, the DesCert project focuses on the assurance-driven development of new software. The DesCert team consists of SRI International, Honeywell Research, and the U…
▽ More
The goal of the DARPA Automated Rapid Certification Of Software (ARCOS) program is to "automate the evaluation of software assurance evidence to enable certifiers to determine rapidly that system risk is acceptable." As part of this program, the DesCert project focuses on the assurance-driven development of new software. The DesCert team consists of SRI International, Honeywell Research, and the University of Washington. We have adopted a formal, tool-based approach to the construction of software artifacts that are supported by rigorous evidence. The DesCert workflow integrates evidence generation into a design process that goes from requirements capture and analysis to the decomposition of the high-level software requirements into architecture properties and software components with assertional contracts, and on to software that can be analyzed both dynamically and statically. The generated evidence is organized by means of an assurance ontology and integrated into the RACK knowledge base.
△ Less
Submitted 28 March, 2022;
originally announced March 2022.
-
Transferable classical force field for pure and mixed metal halide perovskites parameterized from first principles
Authors:
Juan Antonio Seijas-Bellido,
Bipasa Samanta,
Karen Valadez-Villalobos,
Juan Jesús Gallardo,
Javier Navas,
Salvador R. G. Balestra,
Rafael María Madero-Castro,
Jose Manuel Vicent-Luna,
Shuxia Tao,
Maytal Caspary Toroker,
Juan Antonio Anta
Abstract:
Many key features in photovoltaic perovskites occur in relatively long time scales and involve mixed compositions. This requires realistic but also numerically simple models. In this work we present a transferable classical force field to describe the mixed hybrid perovskite MA$_x$FA$_{1-x}$Pb(Br$_y$I$_{1-y}$)$_3$ for variable composition ($\forall x,y \in [0,1]$). The model includes Lennard-Jones…
▽ More
Many key features in photovoltaic perovskites occur in relatively long time scales and involve mixed compositions. This requires realistic but also numerically simple models. In this work we present a transferable classical force field to describe the mixed hybrid perovskite MA$_x$FA$_{1-x}$Pb(Br$_y$I$_{1-y}$)$_3$ for variable composition ($\forall x,y \in [0,1]$). The model includes Lennard-Jones and Buckingham potentials to describe the interactions between the atoms of the inorganic lattice and the organic molecule, and the AMBER model to describe intramolecular atomic interactions. Most of the parameters of the force field have been obtained by means of a genetic algorithm previously developed to parameterize the CsPb(Br$_x$I$_{1-x}$)$_3$ perovskite. The algorithm finds the best parameter set that simultaneously fits the DFT energies obtained for several crystalline structures with moderate degrees of distortion with respect to the equilibrium configuration. The resulting model reproduces correctly the XRD patterns, the expansion of the lattice upon I/Br substitution and the thermal expansion coefficients. We use the model to run classical molecular dynamics simulations with up to 8600 atoms and simulation times of up to 40~ns. From the simulations we have extracted the ion diffusion coefficient of the pure and mixed perovskites, presenting for the first time these values obtained by a fully dynamical method using a transferable model fitted to first principles calculations. The values here reported can be considered as the theoretical upper limit for ion migration dynamics induced by halide vacancies in photovoltaic perovskite devices under operational conditions.
△ Less
Submitted 23 November, 2021;
originally announced November 2021.
-
Experimental Study of the Phase Noise in K-band ARoF systems for Low Complexity 5G receivers
Authors:
Javier Pérez Santacruz,
Simon Rommel,
Antonio Jurado Navas,
Ulf Johannsen,
Idelfonso Tafur Monroy
Abstract:
In this paper, an experimental analysis of the phase noise in an OFDM ARoF setup at 25 GHzfor beyond 5G is presented. The configuration of the setup allows to gradually scale the final phase noise level of the system. Moreover, an OFDM phase noise mitigation method with low complexity and delay is proposed and explained. The proposed method is an advanced version of the LI-CPE algorithm. The advan…
▽ More
In this paper, an experimental analysis of the phase noise in an OFDM ARoF setup at 25 GHzfor beyond 5G is presented. The configuration of the setup allows to gradually scale the final phase noise level of the system. Moreover, an OFDM phase noise mitigation method with low complexity and delay is proposed and explained. The proposed method is an advanced version of the LI-CPE algorithm. The advanced LI-CPE version avoids the one OFDM symbol delay of its antecedent. In addition, the yields of using both methods are shown under different phase noise levels and with different subcarrier spacings. Finally, it is experimentally proven that the proposed method performs better than its previous version.
△ Less
Submitted 15 September, 2021;
originally announced September 2021.
-
Compositional Verification of Smart Contracts Through Communication Abstraction (Extended)
Authors:
Scott Wesley,
Maria Christakis,
Jorge A. Navas,
Richard Trefler,
Valentin Wüstholz,
Arie Gurfinkel
Abstract:
Solidity smart contracts are programs that manage up to 2^160 users on a blockchain. Verifying a smart contract relative to all users is intractable due to state explosion. Existing solutions either restrict the number of users to under-approximate behaviour, or rely on manual proofs. In this paper, we present local bundles that reduce contracts with arbitrarily many users to sequential programs w…
▽ More
Solidity smart contracts are programs that manage up to 2^160 users on a blockchain. Verifying a smart contract relative to all users is intractable due to state explosion. Existing solutions either restrict the number of users to under-approximate behaviour, or rely on manual proofs. In this paper, we present local bundles that reduce contracts with arbitrarily many users to sequential programs with a few representative users. Each representative user abstracts concrete users that are locally symmetric to each other relative to the contract and the property. Our abstraction is semi-automated. The representatives depend on communication patterns, and are computed via static analysis. A summary for the behaviour of each representative is provided manually, but a default summary is often sufficient. Once obtained, a local bundle is amenable to sequential static analysis. We show that local bundles are relatively complete for parameterized safety verification, under moderate assumptions. We implement local bundle abstraction in SmartACE, and show order-of-magnitude speedups compared to a state-of-the-art verifier.
△ Less
Submitted 31 August, 2021; v1 submitted 18 July, 2021;
originally announced July 2021.
-
Automatically Tailoring Static Analysis to Custom Usage Scenarios
Authors:
Muhammad Numair Mansur,
Benjamin Mariano,
Maria Christakis,
Jorge A. Navas,
Valentin Wüstholz
Abstract:
In recent years, there has been significant progress in the development and industrial adoption of static analyzers. Such analyzers typically provide a large, if not huge, number of configurable options controlling the precision and performance of the analysis. A major hurdle in integrating static analyzers in the software-development life cycle is tuning their options to custom usage scenarios, s…
▽ More
In recent years, there has been significant progress in the development and industrial adoption of static analyzers. Such analyzers typically provide a large, if not huge, number of configurable options controlling the precision and performance of the analysis. A major hurdle in integrating static analyzers in the software-development life cycle is tuning their options to custom usage scenarios, such as a particular code base or certain resource constraints. In this paper, we propose a technique that automatically tailors a static analyzer, specifically an abstract interpreter, to the code under analysis and any given resource constraints. We implement this technique in a framework called TAILOR, which we use to perform an extensive evaluation on real-world benchmarks. Our experiments show that the configurations generated by TAILOR are vastly better than the default analysis options, vary significantly depending on the code under analysis, and most remain tailored to several subsequent code versions.
△ Less
Submitted 30 September, 2020; v1 submitted 29 September, 2020;
originally announced September 2020.
-
Unification-based Pointer Analysis without Oversharing
Authors:
Jakub Kuderski,
Jorge A. Navas,
Arie Gurfinkel
Abstract:
Pointer analysis is indispensable for effectively verifying heap-manipulating programs. Even though it has been studied extensively, there are no publicly available pointer analyses that are moderately precise while scalable to large real-world programs. In this paper, we show that existing context-sensitive unification-based pointer analyses suffer from the problem of oversharing -- propagating t…
▽ More
Pointer analysis is indispensable for effectively verifying heap-manipulating programs. Even though it has been studied extensively, there are no publicly available pointer analyses that are moderately precise while scalable to large real-world programs. In this paper, we show that existing context-sensitive unification-based pointer analyses suffer from the problem of oversharing -- propagating too many abstract objects across the analysis of different procedures, which prevents them from scaling to large programs. We present a new pointer analysis for LLVM, called TeaDsa, without such an oversharing. We show how to further improve precision and speed of TeaDsa with extra contextual information, such as flow-sensitivity at call- and return-sites, and type information about memory accesses. We evaluate TeaDsa on the verification problem of detecting unsafe memory accesses and compare it against two state-of-the-art pointer analyses: SVF and SeaDsa. We show that TeaDsa is one order of magnitude faster than either SVF or SeaDsa, strictly more precise than SeaDsa, and, surprisingly, sometimes more precise than SVF.
△ Less
Submitted 16 August, 2019; v1 submitted 4 June, 2019;
originally announced June 2019.
-
Water vapour pressure as determining control parameter to fabricate high efficiency perovskite solar cells at ambient conditions
Authors:
Lidia Contreras-Bernal,
Juan Jesus Gallardo,
Javier Navas,
Jesus Idigoras,
Juan A. Anta
Abstract:
Although perovskite solar cells have demonstrated impressive efficiencies in research labs (above 23%), there is a need of experimental procedures that allow their fabrication at ambient conditions, which would decrease substantially manufacturing costs. However, under ambient conditions, a delicate control of the moisture level in the atmosphere has to be enforced to achieve efficient and highly…
▽ More
Although perovskite solar cells have demonstrated impressive efficiencies in research labs (above 23%), there is a need of experimental procedures that allow their fabrication at ambient conditions, which would decrease substantially manufacturing costs. However, under ambient conditions, a delicate control of the moisture level in the atmosphere has to be enforced to achieve efficient and highly stable devices. In this work, we show that it is the absolute content of water measured in the form of partial water vapour pressure (WVP) the only determining control parameter that needs to be considered during preparation. Following this perspective, MAPbI3 perovskite films were deposited under different WVP by changing the relative humidity (RH) and the lab temperature. We found that efficient and reproducible devices can be obtained at given values of WVP. Furthermore, it is demonstrated that small temperature changes, at the same value of the RH, result in huge changes in performance, due to the non-linear dependence of the WVP on temperature. We have extended the procedure to accomplish high-efficient FA0.83MA0.17PbI3 devices at ambient conditions by adjusting DMSO proportion in precursor solution as a function of WVP only. As an example of the relevance of this paramater, a WVP value of around of 1.6 kPa appears to be an upper limit for safe fabrication of high efficiency devices at ambient conditions, regardless the RH and lab temperature.
△ Less
Submitted 12 February, 2019;
originally announced February 2019.
-
Horn Clauses as an Intermediate Representation for Program Analysis and Transformation
Authors:
Graeme Gange,
Jorge A. Navas,
Peter Schachte,
Harald Sondergaard,
Peter J. Stuckey
Abstract:
Many recent analyses for conventional imperative programs begin by transforming programs into logic programs, capitalising on existing LP analyses and simple LP semantics. We propose using logic programs as an intermediate program representation throughout the compilation process. With restrictions ensuring determinism and single-modedness, a logic program can easily be transformed to machine lang…
▽ More
Many recent analyses for conventional imperative programs begin by transforming programs into logic programs, capitalising on existing LP analyses and simple LP semantics. We propose using logic programs as an intermediate program representation throughout the compilation process. With restrictions ensuring determinism and single-modedness, a logic program can easily be transformed to machine language or other low-level language, while maintaining the simple semantics that makes it suitable as a language for program analysis and transformation. We present a simple LP language that enforces determinism and single-modedness, and show that it makes a convenient program representation for analysis and transformation.
△ Less
Submitted 21 July, 2015;
originally announced July 2015.
-
Verification of Programs by Combining Iterated Specialization with Interpolation
Authors:
Emanuele De Angelis,
Fabio Fioravanti,
Jorge A. Navas,
Maurizio Proietti
Abstract:
We present a verification technique for program safety that combines Iterated Specialization and Interpolating Horn Clause Solving. Our new method composes together these two techniques in a modular way by exploiting the common Horn Clause representation of the verification problem. The Iterated Specialization verifier transforms an initial set of verification conditions by using unfold/fold equiv…
▽ More
We present a verification technique for program safety that combines Iterated Specialization and Interpolating Horn Clause Solving. Our new method composes together these two techniques in a modular way by exploiting the common Horn Clause representation of the verification problem. The Iterated Specialization verifier transforms an initial set of verification conditions by using unfold/fold equivalence preserving transformation rules. During transformation, program invariants are discovered by applying widening operators. Then the output set of specialized verification conditions is analyzed by an Interpolating Horn Clause solver, hence adding the effect of interpolation to the effect of widening. The specialization and interpolation phases can be iterated, and also combined with other transformations that change the direction of propagation of the constraints (forward from the program preconditions or backward from the error conditions). We have implemented our verification technique by integrating the VeriMAP verifier with the FTCLP Horn Clause solver, based on Iterated Specialization and Interpolation, respectively. Our experimental results show that the integrated verifier improves the precision of each of the individual components run separately.
△ Less
Submitted 2 December, 2014;
originally announced December 2014.
-
A Complete Refinement Procedure for Regular Separability of Context-Free Languages
Authors:
Graeme Gange,
Jorge A. Navas,
Peter Schachte,
Harald Sondergaard,
Peter J. Stuckey
Abstract:
Often, when analyzing the behaviour of systems modelled as context-free languages, we wish to know if two languages overlap. To this end, we present an effective semi-decision procedure for regular separability of context-free languages, based on counter-example guided abstraction refinement. We propose two refinement methods, one inexpensive but incomplete, and the other complete but more expensi…
▽ More
Often, when analyzing the behaviour of systems modelled as context-free languages, we wish to know if two languages overlap. To this end, we present an effective semi-decision procedure for regular separability of context-free languages, based on counter-example guided abstraction refinement. We propose two refinement methods, one inexpensive but incomplete, and the other complete but more expensive. We provide an experimental evaluation of this procedure, and demonstrate its practicality on a range of verification and language-theoretic instances.
△ Less
Submitted 19 November, 2014;
originally announced November 2014.
-
A Partial-Order Approach to Array Content Analysis
Authors:
Graeme Gange,
Jorge A. Navas,
Peter Schachte,
Harald Sondergaard,
Peter J. Stuckey
Abstract:
We present a parametric abstract domain for array content analysis. The method maintains invariants for contiguous regions of the array, similar to the methods of Gopan, Reps and Sagiv, and of Halbwachs and Peron. However, it introduces a novel concept of an array content graph, avoiding the need for an up-front factorial partitioning step. The resulting analysis can be used with arbitrary numeric…
▽ More
We present a parametric abstract domain for array content analysis. The method maintains invariants for contiguous regions of the array, similar to the methods of Gopan, Reps and Sagiv, and of Halbwachs and Peron. However, it introduces a novel concept of an array content graph, avoiding the need for an up-front factorial partitioning step. The resulting analysis can be used with arbitrary numeric relational abstract domains; we evaluate the domain on a range of array manipulating program fragments.
△ Less
Submitted 7 August, 2014;
originally announced August 2014.
-
Symbolic Execution for Verification
Authors:
Joxan Jaffar,
Jorge A. Navas,
Andrew E. Santosa
Abstract:
In previous work, we presented a symbolic execution method which starts with a concrete model of the program but progressively abstracts away details only when these are known to be irrelevant using interpolation. In this paper, we extend the technique to handle unbounded loops. The central idea is to progressively discover the strongest invariants through a process of loop unrolling. The key feat…
▽ More
In previous work, we presented a symbolic execution method which starts with a concrete model of the program but progressively abstracts away details only when these are known to be irrelevant using interpolation. In this paper, we extend the technique to handle unbounded loops. The central idea is to progressively discover the strongest invariants through a process of loop unrolling. The key feature of this technique, called the minimax algorithm, is intelligent backtracking which directs the search for the next invariant. We then present an analysis of the main differences between our symbolic execution method and mainstream techniques mainly based on abstract refinement (CEGAR). Finally, we evaluate our technique against available state-of-the-art systems.
△ Less
Submitted 10 March, 2011;
originally announced March 2011.
-
Towards Parameterized Regular Type Inference Using Set Constraints
Authors:
F. Bueno,
J. Navas,
M. Hermenegildo
Abstract:
We propose a method for inferring \emph{parameterized regular types} for logic programs as solutions for systems of constraints over sets of finite ground Herbrand terms (set constraint systems). Such parameterized regular types generalize \emph{parametric} regular types by extending the scope of the parameters in the type definitions so that such parameters can relate the types of different pre…
▽ More
We propose a method for inferring \emph{parameterized regular types} for logic programs as solutions for systems of constraints over sets of finite ground Herbrand terms (set constraint systems). Such parameterized regular types generalize \emph{parametric} regular types by extending the scope of the parameters in the type definitions so that such parameters can relate the types of different predicates. We propose a number of enhancements to the procedure for solving the constraint systems that improve the precision of the type descriptions inferred. The resulting algorithm, together with a procedure to establish a set constraint system from a logic program, yields a program analysis that infers tighter safe approximations of the success types of the program than previous comparable work, offering a new and useful efficiency vs. precision trade-off. This is supported by experimental results, which show the feasibility of our analysis.
△ Less
Submitted 9 February, 2010;
originally announced February 2010.
-
Consumption and Portfolio Rules for Time-Inconsistent Investors
Authors:
Jesus Marin-Solano,
Jorge Navas
Abstract:
This paper extends the classical consumption and portfolio rules model in continuous time (Merton 1969, 1971) to the framework of decision-makers with time-inconsistent preferences. The model is solved for different utility functions for both, naive and sophisticated agents, and the results are compared. In order to solve the problem for sophisticated agents, we derive a modified HJB (Hamilton-J…
▽ More
This paper extends the classical consumption and portfolio rules model in continuous time (Merton 1969, 1971) to the framework of decision-makers with time-inconsistent preferences. The model is solved for different utility functions for both, naive and sophisticated agents, and the results are compared. In order to solve the problem for sophisticated agents, we derive a modified HJB (Hamilton-Jacobi-Bellman) equation. It is illustrated how for CRRA functions within the family of HARA functions (logarithmic and potential cases) the optimal portfolio rule does not depend on the discount rate, but this is not the case for a general utility function, such as the exponential (CARA) utility function.
△ Less
Submitted 27 March, 2009; v1 submitted 16 January, 2009;
originally announced January 2009.
-
Science with the new generation high energy gamma- ray experiments
Authors:
M. Alvarez,
D. D'Armiento,
G. Agnetta,
A. Alberdi,
A. Antonelli,
A. Argan,
P. Assis,
E. A. Baltz,
C. Bambi,
G. Barbiellini,
H. Bartko,
M. Basset,
D. Bastieri,
P. Belli,
G. Benford,
L. Bergstrom,
R. Bernabei,
G. Bertone,
A. Biland,
B. Biondo,
F. Bocchino,
E. Branchini,
M. Brigida,
T. Bringmann,
P. Brogueira
, et al. (175 additional authors not shown)
Abstract:
This Conference is the fifth of a series of Workshops on High Energy Gamma- ray Experiments, following the Conferences held in Perugia 2003, Bari 2004, Cividale del Friuli 2005, Elba Island 2006. This year the focus was on the use of gamma-ray to study the Dark Matter component of the Universe, the origin and propagation of Cosmic Rays, Extra Large Spatial Dimensions and Tests of Lorentz Invaria…
▽ More
This Conference is the fifth of a series of Workshops on High Energy Gamma- ray Experiments, following the Conferences held in Perugia 2003, Bari 2004, Cividale del Friuli 2005, Elba Island 2006. This year the focus was on the use of gamma-ray to study the Dark Matter component of the Universe, the origin and propagation of Cosmic Rays, Extra Large Spatial Dimensions and Tests of Lorentz Invariance.
△ Less
Submitted 4 December, 2007;
originally announced December 2007.
-
GAW - An Imaging Atmospheric Cherenkov Telescope with Large Field of View
Authors:
G. Cusumano,
G. Agnetta,
A. Alberdi,
M. Alvarez,
P. Assis,
B. Biondo,
F. Bocchino,
P. Brogueira,
J. A. Caballero,
M. Carvajal,
A. J. Castro-Tirado,
O. Catalano,
F. Celi,
C. Delgado,
G. Di Cocco,
A. Dominguez,
J. M. Espino Navas,
M. C. Espirito Santo,
M. I. Gallardo,
J. E. Garcia,
S. Giarrusso,
M. Gomez,
J. L. Gomez,
P. Goncalves,
M. Guerriero
, et al. (25 additional authors not shown)
Abstract:
GAW, acronym for Gamma Air Watch, is a Research and Development experiment in the TeV range, whose main goal is to explore the feasibility of large field of view Imaging Atmospheric Cherenkov Telescopes. GAW is an array of three relatively small telescopes (2.13 m diameter) which differs from the existing and presently planned projects in two main features: the adoption of a refractive optics sy…
▽ More
GAW, acronym for Gamma Air Watch, is a Research and Development experiment in the TeV range, whose main goal is to explore the feasibility of large field of view Imaging Atmospheric Cherenkov Telescopes. GAW is an array of three relatively small telescopes (2.13 m diameter) which differs from the existing and presently planned projects in two main features: the adoption of a refractive optics system as light collector and the use of single photoelectron counting as detector working mode. The optics system allows to achieve a large field of view (24x24 squared degrees) suitable for surveys of large sky regions. The single photoelectron counting mode in comparison with the charge integration mode improves the sensitivity by permitting also the reconstruction of events with a small number of collected Cherenkov photons. GAW, which is a collaboration effort of Research Institutes in Italy, Portugal and Spain, will be erected in the Calar Alto Observatory (Sierra de Los Filabres - Andalucia, Spain), at 2150 m a.s.l.). The first telescope will be settled within Autumn 2007. This paper shows the main characteristics of the experiment and its expected performance.
△ Less
Submitted 31 July, 2007;
originally announced July 2007.
-
A study of set-sharing analysis via cliques
Authors:
Jorge Navas,
Francisco Bueno,
Manuel Hermenegildo
Abstract:
We study the problem of efficient, scalable set-sharing analysis of logic programs. We use the idea of representing sharing information as a pair of abstract substitutions, one of which is a worst-case sharing representation called a clique set, which was previously proposed for the case of inferring pair-sharing. We use the clique-set representation for (1) inferring actual set-sharing informat…
▽ More
We study the problem of efficient, scalable set-sharing analysis of logic programs. We use the idea of representing sharing information as a pair of abstract substitutions, one of which is a worst-case sharing representation called a clique set, which was previously proposed for the case of inferring pair-sharing. We use the clique-set representation for (1) inferring actual set-sharing information, and (2) analysis within a top-down framework. In particular, we define the abstract functions required by standard top-down analyses, both for sharing alone and also for the case of including freeness in addition to sharing. Our experimental evaluation supports the conclusion that, for inferring set-sharing, as it was the case for inferring pair-sharing, precision losses are limited, while useful efficiency gains are obtained. At the limit, the clique-set representation allowed analyzing some programs that exceeded memory capacity using classical sharing representations.
△ Less
Submitted 25 August, 2005;
originally announced August 2005.
