On model checking multiple hybrid views

Many applications, for instance the MS .NET Global Assembly Cache (GAC), are naturally expressed as 3-valued models where an additional third truth value models uncertainty or under-specification. An example of under-specification is that a component in a GAC may or may not have a main method. Models described in this manner can then be analyzed to refute or verify properties about the concrete systems they intend to model. This approach to system validation traditionally considers only one model at a time, even though this model may evolve if subjected to analysis. Many applications, however, benefit from or require the simultaneous consideration of multiple models of systems. We mention here requirements from different stake holders, and data drawn from federated databases.     

Modeling and predicting the popularity of online contents with Cox proportional hazard regression model

We propose a general framework which can be used for modeling and predicting the popularity of online contents. The aim of our modeling is not inferring the precise popularity value of a content, but inferring the likelihood with which the content will be popular. Our approach is rooted in survival analysis which deals with the survival time until an event of a failure or death. Survival analysis assumes that predicting the precise lifetime of an instance is very hard but predicting the likelihood of the lifetime of an instance is possible based on its hazard distribution. Additionally we position ourselves in the standpoint of an external observer who has to model the popularity of contents only with publicly available information. Thus, the goal of our proposed methodology is to model a certain popularity metric, such as the lifetime of a content and the number of comments which a content receives, with a set of explanatory factors, which are observable by the external observer.Among various parametric and non-parametric approaches for the survival analysis, we use the Cox proportional hazard regression model, which divides the distribution function of a certain popularity metric into two components: one which is explained by a set of explanatory factors, called risk factors, and another, a baseline survival distribution function, which integrates all the factors not taken into account. In order to validate our proposed methodology, we use two datasets crawled from two different discussion forums, forum.dpreview.com and forums.myspace.com, which are one of the largest discussion forum dealing various issues on digital cameras and a discussion forum provided by a representative social networks. We model two difference popularity metrics, the lifetime of threads and the number of comments, and we show that the models can predict the lifetime of threads from Dpreview (Myspace) by observing a thread during the first 5-6 days (24 h, respectively) and the number of comments of Dpreview threads by observing a thread during first 2-3 days.     

Symbolic expansion of transcendental functions

Higher transcendental function occur frequently in the calculation of Feynman integrals in quantum field theory. Their expansion in a small parameter is a non-trivial task. We report on a computer program which allows the systematic expansion of certain classes of functions. The algorithms are based on the Hopf algebra of nested sums. The program is written in C++ and uses the GiNaC library.     

程序模型检查器综述

模型检查实际程序设计语言编写的程序是近年来程序验证领域的研究热点之一,出现了一批针对C,C++或Java语言的程序模型检查器原型.总结了程序模型检查中的主要问题及相关技术,以是否使用中间建模语言为标准,对现有程序模型检查器进行了分类,并具体地介绍了一些代表性工具中的模型获取及化简技术,最后展望了程序模型检查器未来的研究方向.     

Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite

This paper is a case study in combining theorem provers. We define a derived rule in HOL-Light, CVC_PROVE, which calls CVC Lite and translates the resulting proof object back to HOL-Light. As a result, we obtain a highly trusted proof-checker for CVC Lite, while also fundamentally expanding the capabilities of HOL-Light.     

eHDECAY: An implementation of the Higgs effective Lagrangian into HDECAY

We present eHDECAY, a modified version of the program HDECAY which includes the full list of leading bosonic operators of the Higgs effective Lagrangian with a linear or non-linear realization of the electroweak symmetry and implements two benchmark composite Higgs models.     

Extended rate, more GFUN

We present a software package that guesses formulae for sequences of, for example, rational numbers or rational functions, given the first few terms. We implement an algorithm due to Bernhard Beckermann and George Labahn, together with some enhancements to render our package efficient. Thus we extend and complement Christian Krattenthaler’s program Rate.m, the parts concerned with guessing of Bruno Salvy and Paul Zimmermann’s GFUN, the univariate case of Manuel Kauers’ Guess.m and Manuel Kauers’ and Christoph Koutschan’s qGeneratingFunctions.m.     

A Bayesian analysis of the thermal challenge problem

A major question for the application of computer models is Does the computer model adequately represent reality? Viewing the computer models as a potentially biased representation of reality, Bayarri et al. [M. Bayarri, J. Berger, R. Paulo, J. Sacks, J. Cafeo, J. Cavendish, C. Lin, J. Tu, A framework for validation of computer models, Technometrics 49 (2) (2007) 138–154] develop the simulator assessment and validation engine (SAVE) method as a general framework for answering this question. In this paper, we apply the SAVE method to the challenge problem which involves a thermal computer model designed for certain devices. We develop a statement of confidence that the devices modeled can be applied in intended situations.     

How does a box work? A study in the qualitative dynamics of solid objects

This paper is an in-depth study of qualitative physical reasoning about one particular scenario: using a box to carry a collection of objects from one place to another. Specifically we consider the plan, plan1 “Load objects uCargo into box oBox one by one; carry oBox from location l1 to location l2”. We present qualitative constraints on the shape, starting position, and material properties of uCargo and oBox and on the characteristics of the motion that suffice to make it virtually certain that plan1 can be successfully executed. We develop a theory, consisting mostly of first-order statements together with two default rules, that supports an inference of the form “If conditions XYZ hold, and the agent attempts to carry out plan1 then presumably he will succeed”. Our theory is elaboration tolerant in the sense that carrying out the analogous inference for carrying objects in boxes with lids, in boxes with small holes, or on trays can reuse much of the same knowledge. The theory integrates reasoning about continuous time, Euclidean space, commonsense dynamics of solid objects, and semantics of partially specified plans.     

Top++: A program for the calculation of the top-pair cross-section at hadron colliders

We present the program Top++ for the numerical evaluation of the total inclusive cross-section for producing top quark pairs at hadron colliders. The program calculates the cross-section in (a) fixed order approach with exact next-to-next-to leading order (NNLO) accuracy and (b) by including soft-gluon resummation for the hadronic cross-section in Mellin space with full next-to-next-to-leading logarithmic (NNLL) accuracy. The program offers the user significant flexibility through the large number (29) of available options. Top++ is written in C++. It has a very simple to use interface that is intuitive and directly reflects the physics. The running of the program requires no programming experience from the user.     

Automated Fault Localization for C Programs

If a program does not fulfill a given specification, a model checker delivers a counterexample, a run which demonstrates the wrong behavior. Even with a counterexample, locating the actual fault in the source code is often a difficult task for the verification engineer.We present an automatic approach for fault localization in C programs. The method is based on model checking and reports only components that can be changed such that the difference between actual and intended behavior of the example is removed. To identify these components, we use the bounded model checker CBMC on an instrumented version of the program. We present experimental data that supports the applicability of our approach.     

An updated version of wannier90: A tool for obtaining maximally-localised Wannier functions

wannier90  is a program for calculating maximally-localised Wannier functions (MLWFs) from a set of Bloch energy bands that may or may not be attached to or mixed with other bands. The formalism works by minimising the total spread of the MLWFs in real space. This is done in the space of unitary matrices that describe rotations of the Bloch bands at each k-point. As a result, wannier90  is independent of the basis set used in the underlying calculation to obtain the Bloch states. Therefore, it may be interfaced straightforwardly to any electronic structure code. The locality of MLWFs can be exploited to compute band-structure, density of states and Fermi surfaces at modest computational cost. Furthermore, wannier90  is able to output MLWFs for visualisation and other post-processing purposes. Wannier functions are already used in a wide variety of applications. These include analysis of chemical bonding in real space; calculation of dielectric properties via the modern theory of polarisation; and as an accurate and minimal basis set in the construction of model Hamiltonians for large-scale systems, in linear-scaling quantum Monte Carlo calculations, and for efficient computation of material properties, such as the anomalous Hall coefficient. We present here an updated version of wannier90, wannier90  2.0, including minor bug fixes and parallel (MPI) execution for band-structure interpolation and the calculation of properties such as density of states, Berry curvature and orbital magnetisation. wannier90  is freely available under the GNU General Public License from http://www.wannier.org/.     

Light Dialectica Program Extraction from a Classical Fibonacci Proof

We demonstrate program extraction by the Light Dialectica Interpretation (LDI) on a minimal logic proof of the classical existence of Fibonacci numbers. This semi-classical proof is available in MinLog's library of examples. The term of Gödel's T extracted by the LDI is, after strong normalization, exactly the usual recursive algorithm which defines the Fibonacci numbers (in pairs). This outcome of the Light Dialectica meta-algorithm is much better than the T-program extracted by means of the pure Gödel Dialectica Interpretation. It is also strictly less complex than the result obtained by means of the refined A-translation technique of Berger, Buchholz and Schwichtenberg on an artificially distorted variant of the input proof, but otherwise it is identical with the term yielded by Berger's Kripke-style refined A-translation. Although syntactically different, it also has the same computational complexity as the original program yielded by the refined A-translation from the undistorted input classical Fibonacci proof.     

Practical Datatype Specializations with Phantom Types and Recursion Schemes

Datatype specialization is a form of subtyping that captures program invariants on data structures that are expressed using the convenient and intuitive datatype notation. Of particular interest are structural invariants such as well-formedness. We investigate the use of phantom types for describing datatype specializations. We show that it is possible to express statically-checked specializations within the type system of Standard ML. We also show that this can be done in a way that does not lose useful programming facilities such as pattern matching in case expressions.     

Using XBDDs and ZBDDs in points‐to analysis

Binary decision diagrams (BDDs) have recently become widely accepted as a space‐efficient method of representing relations in points‐to or reference analyses. When BDDs are used to represent relations, each element of a domain is assigned a bit pattern to represent it, but not every bit pattern represents an element. The circuit design, model checking, and verification communities have achieved significant reductions in BDD sizes using several techniques to reduce the overhead of these don't‐care bit patterns. We adapt these techniques to BDD‐based program analysis, and we study their effect on the BDD size in this context. Specifically, we compare the effectiveness of Coudert and Madre's restrict operation and the use of zero‐suppressed BDDs (ZBDDs) to represent relations. Using don't‐care BDDs (XBDDs) and ZBDDs to reduce the size of the relations allows a compiler or other software analysis tools to analyze larger programs with greater precision. Our experimental evaluation considers both context‐insensitive and context‐sensitive program analyses. We also provide a metric that can be used to estimate whether ZBDDs will be more compact than BDDs for a given analysis. Copyright © 2008 John Wiley & Sons, Ltd.     

The tauola-photos-F environment for the TAUOLA and PHOTOS packages, release II

We present the system for maintaining the versions of two packages: the TAUOLA of τ-lepton decay and PHOTOS for radiative corrections in decays. The following features can be chosen in an automatic or semi-automatic way: (1) format of the common block HEPEVT; (2) version of the physics input (for TAUOLA): as published, as initialized by the CLEO collaboration, as initialized by the ALEPH collaboration (it is suggested to use this version only with the help of the collaboration advice), new optional parametrization of matrix elements in 4π decay channels; (3) type of application: stand-alone, universal interface based on the information stored in the HEPEVT common block including longitudinal spin effects in the elementary Z/γ^∗→τ⁺τ⁻ process, extended version of the standard universal interface including full spin effects in the H/A→τ⁺τ⁻ decay, interface for KKMC Monte Carlo, (4) random number generators; (5) compiler options. The last section of the paper contains documentation of the programs updates introduced over the last two years.

Program summary

Title of program:tauola-photos-F, release IICatalogue identifier:ADXO_v1_0Program summary URL:http://cpc.cs.qub.ac.uk/summaries/ADXO_v1_0Programs obtainable from: CPC Program Library, Queen's University of Belfast, N. IrelandComputer: PC running GNU/Linux operating systemProgramming languages and tools used:CPP: standard C-language preprocessor, GNU Make builder tool, also FORTRAN compilerNo. of lines in distributed program, including test data, etc.: 194 118No. of bytes in distributed program, including test data, etc.:2 481 234Distribution format: tar.gzCatalogue identifier:ADXO_v2_0Program summary URL:http://cpc.cs.qub.ac.uk/summaries/ADXO_v2_0No. of lines in distributed program, including test data, etc.:308 235No. of bytes in distributed program, including test data, etc.:2 988 363Distribution format:tar.gzDoes the new version supersede the previous version:YesNature of the physical problem: The code of Monte Carlo generators often has to be tuned to the needs of large HEP Collaborations and experiments. Usually, these modifications do not introduce important changes in the algorithm, but rather modify the initialization and form of the hadronic current in τ decays. The format of the event record (HEPEVT common block) used to exchange information between building blocks of Monte Carlo systems often needs modification. Thus, there is a need to maintain various, slightly modified versions of the same code. The package presented here allows the production of ready-to-compile versions of TAUOLA [S. Jadach, Z. Wa?s, R. Decker, J.H. Kühn, Comput. Phys. Comm. 76 (1993) 361; A.E. Bondar, et al., Comput. Phys. Comm. 146 (2002) 139] and PHOTOS [E. Barberio, Z. Wa?s, Comput. Phys. Comm. 79 (1994) 291] Monte Carlo generators with appropriate demonstration programs. The new algorithm, universal interface of TAUOLA to work with the HEPEVT common block, is also documented here. Finally, minor technical improvements of TAUOLA and PHOTOS are also listed.Method of solution: The standard UNIX tool: the C-language preprocessor is used to produce a ready-to-distribute version of TAUOLA and PHOTOS code. The final FORTRAN code is produced from the library of ‘pre-code’ that is included in the package.Reasons for new version: The functionality of the version of TAUOLA and PHOTOS changed over the last two years. The changes, and their reasons, are documented in Section 9, and our new papers cited in this section.Additional comments: The updated version includes new features described in Section 9 of the paper. PHOTOS and TAUOLA were first submitted to the library as separate programs. Summary details of these previous programs are obtainable from the CPC Program Library.Typical running time: Depends on the speed of the computer used and the demonstration program chosen. Typically a few seconds.     

GYutsis: heuristic based calculation of general recoupling coefficients

General angular momentum recoupling coefficients can be expressed as a summation formula over products of 6-j coefficients. Yutsis, Levinson and Vanagas developed graphical techniques for representing the general recoupling coefficient as a cubic graph and they describe a set of reduction rules allowing a stepwise generation of the corresponding summation formula. This paper is a follow up to [Van Dyck and Fack, Comput. Phys. Comm. 151 (2003) 353-368] where we described a heuristic algorithm based on these techniques. In this article we separate the heuristic from the algorithm and describe some new heuristic approaches which can be plugged into the generic algorithm. We show that these new heuristics lead to good results: in many cases we get a more efficient summation formula than our previous approach, in particular for problems of higher order. In addition the new features and the use of our program GYutsis, which implements these techniques, is described both for end users and application programmers.

Program summary

Title of program: CycleCostAlgorithm, GYutsisCatalogue number: ADSAProgram Summary URL:http://cpc.cs.qub.ac.uk/summaries/ADSAProgram obtainable from: CPC Program Library, Queen's University of Belfast, N. Ireland. Users may obtain the program also by downloading either the compressed tar file gyutsis.tgz (for Unix and Linux) or the zip file gyutsis.zip (for Windows) from our website (http://caagt.rug.ac.be/yutsis/). An applet version of the program is also available on our website and can be run in a web browser from the URL http://caagt.rug.ac.be/yutsis/GYutsisApplet.html.Licensing provisions: noneComputers for which the program is designed: any computer with Sun's Java Runtime Environment 1.4 or higher installed.Programming language used: Java 1.2 (Compiler: Sun's SDK 1.4.0)No. of lines in program: approximately 9400No. of bytes in distributed program, including test data, etc.: 544 117Distribution format: tar gzip fileNature of physical problem: A general recoupling coefficient for an arbitrary number of (integer or half-integer) angular momenta can be expressed as a formula consisting of products of 6-j coefficients summed over a certain number of variables. Such a formula can be generated using the program GYutsis (with a graphical user front end) or CycleCostAlgorithm (with a text-mode user front end).Method of solution: Using the graphical techniques of Yutsis, Levinson and Vanagas (1962) a summation formula for a general recoupling coefficient is obtained by representing the coefficient as a Yutsis graph and by performing a selection of reduction rules valid for such graphs. Each reduction rule contributes to the final summation formula by a numerical factor or by an additional summation variable. Whereas an optimal summation formula (i.e. with a minimum number of summation variables) is hard to obtain, we present here some new heuristic approaches for selecting an edge from a k-cycle in order to transform it into an (k−1)-cycle (k>3) in such a way that a ‘good’ summation formula is obtained.Typical running time: From instantaneously for the typical problems to 30 s for the heaviest problems on a Pentium II-350 Linux-system with 256 MB RAM.     

OptaDOS: A tool for obtaining density of states,core-level and optical spectra from electronic structure codes

We present OptaDOS, a program for calculating core-electron and low-loss electron energy loss spectra (EELS) and optical spectra along with total-, projected- and joint-density of electronic states (DOS) from single-particle eigenenergies and dipole transition coefficients. Energy-loss spectroscopy is an important tool for probing bonding within a material. Interpreting these spectra can be aided by first principles calculations. The spectra are generated from the eigenenergies through integration over the Brillouin zone. An important feature of this code is that this integration is performed using a choice of adaptive or linear extrapolation broadening methods which we show produces higher accuracy spectra than standard fixed-width Gaussian broadening. OptaDOS  may be straightforwardly interfaced to any electronic structure code. OptaDOS  is freely available under the GNU General Public licence from http://www.optados.org.     

A computer program for two-particle generalized coefficients of fractional parentage

We present a FORTRAN90 program GCFP for the calculation of the generalized coefficients of fractional parentage (generalized CFPs or GCFP). The approach is based on the observation that the multi-shell CFPs can be expressed in terms of single-shell CFPs, while the latter can be readily calculated employing a simple enumeration scheme of antisymmetric A-particle states and an efficient method of construction of the idempotent matrix eigenvectors. The program provides fast calculation of GCFPs for a given particle number and produces results possessing numerical uncertainties below the desired tolerance. A single j-shell is defined by four quantum numbers, (e,l,j,t).A supplemental C++ program parGCFP allows calculation to be done in batches and/or in parallel.

Program summary

Program title:GCFP, parGCFPCatalogue identifier: AEBI_v1_0Program summary URL:http://cpc.cs.qub.ac.uk/summaries/AEBI_v1_0.htmlProgram obtainable from: CPC Program Library, Queen's University, Belfast, N. IrelandLicensing provisions: Standard CPC licence, http://cpc.cs.qub.ac.uk/licence/licence.htmlNo. of lines in distributed program, including test data, etc.: 17 199No. of bytes in distributed program, including test data, etc.: 88 658Distribution format: tar.gzProgramming language: FORTRAN 77/90 (GCFP), C++ (parGCFP)Computer: Any computer with suitable compilers. The program GCFP requires a FORTRAN 77/90 compiler. The auxiliary program parGCFP requires GNU-C++ compatible compiler, while its parallel version additionally requires MPI-1 standard librariesOperating system: Linux (Ubuntu, Scientific) (all programs), also checked on Windows XP (GCFP, serial version of parGCFP)RAM: The memory demand depends on the computation and output mode. If this mode is not 4, the program GCFP demands the following amounts of memory on a computer with Linux operating system. It requires around 2 MB of RAM for the A=12 system at Ex?2. Computation of the A=50 particle system requires around 60 MB of RAM at Ex=0 and ∼70 MB at Ex=2 (note, however, that the calculation of this system will take a very long time). If the computation and output mode is set to 4, the memory demands by GCFP are significantly larger. Calculation of GCFPs of A=12 system at Ex=1 requires 145 MB. The program parGCFP requires additional 2.5 and 4.5 MB of memory for the serial and parallel version, respectively.Classification: 17.18Nature of problem: The program GCFP generates a list of two-particle coefficients of fractional parentage for several j-shells with isospin.Solution method: The method is based on the observation that multishell coefficients of fractional parentage can be expressed in terms of single-shell CFPs [1]. The latter are calculated using the algorithm [2,3] for a spectral decomposition of an antisymmetrization operator matrix Y. The coefficients of fractional parentage are those eigenvectors of the antisymmetrization operator matrix Y that correspond to unit eigenvalues. A computer code for these coefficients is available [4]. The program GCFP offers computation of two-particle multishell coefficients of fractional parentage. The program parGCFP allows a batch calculation using one input file. Sets of GCFPs are independent and can be calculated in parallel.Restrictions:A<86 when Ex=0 (due to the memory constraints); small numbers of particles allow significantly higher excitations, though the shell with j?11/2 cannot get full (it is the implementation constraint).Unusual features: Using the program GCFP it is possible to determine allowed particle configurations without the GCFP computation. The GCFPs can be calculated either for all particle configurations at once or for a specified particle configuration. The values of GCFPs can be printed out with a complete specification in either one file or with the parent and daughter configurations printed in separate files. The latter output mode requires additional time and RAM memory. It is possible to restrict the (J,T) values of the considered particle configurations. (Here J is the total angular momentum and T is the total isospin of the system.) The program parGCFP produces several result files the number of which equals to the number of particle configurations. To work correctly, the program GCFP needs to be compiled to read parameters from the standard input (the default setting).Running time: It depends on the size of the problem. The minimum time is required, if the computation and output mode (CompMode) is not 4, but the resulting file is larger. A system with A=12 particles at Ex=0 (all 9411 GCFPs) took around 1 sec on a Pentium4 2.8 GHz processor with 1 MB L2 cache. The program required about 14 min to calculate all 1.3×¹⁰⁶ GCFPs of Ex=1. The time for all 5.5×¹⁰⁷ GCFPs of Ex=2 was about 53 hours. For this number of particles, the calculation time of both Ex=0 and Ex=1 with CompMode = 1 and 4 is nearly the same, when no other processes are running. The case of Ex=2 could not be calculated with CompMode = 4, because the RAM memory was insufficient. In general, the latter CompMode requires a longer computation time, although the resulting files are smaller in size. The program parGCFP puts virtually no time overhead. Its parallel version speeds-up the calculation. However, the results need to be collected from several files created for each configuration.References:[1] J. Levinsonas, Works of Lithuanian SSR Academy of Sciences 4 (1957) 17.[2] A. Deveikis, A. Bon?kus, R. Kalinauskas, Lithuanian Phys. J. 41 (2001) 3.[3] A. Deveikis, R.K. Kalinauskas, B.R. Barrett, Ann. Phys. 296 (2002) 287.[4] A. Deveikis, Comput. Phys. Comm. 173 (2005) 186. (CPC Catalogue ID. ADWI_v1_0)