Reduze - Feynman integral reduction in C++

Reduze is a computer program for reducing Feynman integrals to master integrals employing a Laporta algorithm. The program is written in C++ and uses classes provided by the GiNaC library to perform the simplifications of the algebraic prefactors in the system of equations. Reduze offers the possibility to run reductions in parallel.

Program summary

Program title:ReduzeCatalogue identifier: AEGE_v1_0Program summary URL:http://cpc.cs.qub.ac.uk/summaries/AEGE_v1_0.htmlProgram obtainable from: CPC Program Library, Queen's University, Belfast, N. IrelandLicensing provisions:: yesNo. of lines in distributed program, including test data, etc.: 55 433No. of bytes in distributed program, including test data, etc.: 554 866Distribution format: tar.gzProgramming language: C++Computer: AllOperating system: Unix/LinuxNumber of processors used: The number of processors is problem dependent. More than one possible but not arbitrary many.RAM: Depends on the complexity of the system.Classification: 4.4, 5External routines: CLN (http://www.ginac.de/CLN/), GiNaC (http://www.ginac.de/)Nature of problem: Solving large systems of linear equations with Feynman integrals as unknowns and rational polynomials as prefactors.Solution method: Using a Gauss/Laporta algorithm to solve the system of equations.Restrictions: Limitations depend on the complexity of the system (number of equations, number of kinematic invariants).Running time: Depends on the complexity of the system.     

A new symbolic calculus for the response of nonlinear systems

We present a new operational calculus for computing the response of nonlinear systems to various deterministic excitations. The use of a new tool: noncommutative generating power series, allows us to derive, by simple algebraic manipulations, the Volterra functional series of the solution of a large class of nonlinear forced differential equations. The symbolic calculus introduced appears as a natural generalization to the nonlinear domain, of the well known Heaviside operational calculus. Moreover, this method has the advantage of allowing the use of a computer.     

FeynDyn: A MATLAB program for fast numerical Feynman integral calculations for open quantum system dynamics on GPUs

This MATLAB program calculates the dynamics of the reduced density matrix of an open quantum system modeled either by the Feynman–Vernon model or the Caldeira–Leggett model. The user gives the program a Hamiltonian matrix that describes the open quantum system as if it were in isolation, a matrix of the same size that describes how that system couples to its environment, and a spectral distribution function and temperature describing the environment’s influence on it, in addition to the open quantum system’s initial density matrix and a grid of times. With this, the program returns the reduced density matrix of the open quantum system at all moments specified by that grid of times (or just the last moment specified by the grid of times if the user makes this choice). This overall calculation can be divided into two stages: the setup of the Feynman integral, and the actual calculation of the Feynman integral for time propagation of the density matrix. When this program calculates this propagation on a multi-core CPU, it is this propagation that is usually the rate-limiting step of the calculation, but when it is calculated on a GPU, the propagation is calculated so quickly that the setup of the Feynman integral can actually become the rate-limiting step. The overhead of transferring information from the CPU to the GPU and back seems to have a negligible effect on the overall runtime of the program. When the required information cannot fit on the GPU, the user can choose to run the entire program on a CPU.     

One Head Machines from a symbolic approach

We consider the Turing Machine as a dynamical system and we study a particular partition projection of it. In this way, we define a language (a subshift) associated to each machine. The classical definition of Turing Machines over a one-dimensional tape is generalized to allow for a tape in the form of a Cayley Graph. We study the complexity of the language of a machine in terms of realtime recognition by putting it in relation with the structure of its tape. In this way, we find a large set of realtime subshifts some of which are proved not to be deterministic in realtime. Sofic subshifts of this class correspond to machines that cannot make arbitrarily large tours. We prove that these machines always have an ultimately periodic behavior when starting with a periodic initial configuration, and this result is proved for any Cayley Graph.     

FIRE4, LiteRed and accompanying tools to solve integration by parts relations

We present the new version of the Mathematica code FIRE and ideas behind it. It can be applied together with the recently developed code LiteRed by Lee in order to provide an integration by parts reduction to master integrals for quite complicated families of Feynman integrals. As an example, we consider four-loop massless propagator integrals for which LiteRed provides reduction rules and FIRE assists to apply these rules. So, as a by-product one obtains a four-loop variant of the well-known algorithm MINCER. The existence of these explicit reduction rules shows that any four-loop massless propagator integral can be reduced to a linear combination of master integrals in the sense of a mathematical theorem. We also describe various algebraic ways to find additional relations between master integrals associated with several families of Feynman integrals.     

A refined difference field theory for symbolic summation

In this article we present a refined summation theory based on Karr’s difference field approach. The resulting algorithms find sum representations with optimal nested depth. For instance, the algorithms have been applied successively to evaluate Feynman integrals from Perturbative Quantum Field Theory.     

Processes as formal power series: A coinductive approach to denotational semantics

We characterize must testing equivalence on CSP in terms of the unique homomorphism from the Moore automaton of CSP processes to the final Moore automaton of partial formal power series over a certain semiring. The final automaton is then turned into a CSP-algebra: operators and fixpoints are defined, respectively, via behavioural differential equations and simulation relations. This structure is then shown to be preserved by the final homomorphism. As a result, we obtain a fully abstract compositional model of CSP phrased in purely set-theoretical terms.     

基于多线程并行的符号执行引擎设计与实现

符号执行作为一种高效的测试生成技术,被广泛应用于软件测试、安全分析等领域. 然而,由于程序中的执行路径数量随着分支数量的增加而指数级上升,符号执行往往无法在大规模程序上进行高效执行,缺乏可扩展性. 已有的基于多进程的并行化方法具有较大的额外通信开销,并且缺乏对现有约束求解优化技术的利用. 提出了基于多线程并行处理模型的符号执行加速方法. 具体来讲,为解决并行符号执行中的不同工作节点负载不平衡问题,设计了不需要中间节点参与的工作窃取算法. 为充分利用现有约束求解优化技术,提出了让不同工作节点共享约束求解信息的加速求解方法. 基于符号执行引擎（KLEE）实现了多线程并行化符号执行方案,从而形成多线程并行化符号执行引擎（PKLEE）. 实验验证表明,在穷尽执行路径场景下,KLEE平均耗时是在给定8个线程下PKLEE的3~4倍;在同样的时间内,PKLEE执行的有效工作负载平均是KLEE的3倍.

     

A reification calculus for model-oriented software specification

This paper presents a transformational approach to the derivation of implementations from model-oriented specifications of abstract data types.The purpose of this research is to reduce the number of formal proofs required in model refinement, which hinder software development. It is shown to be applicable to the transformation of models written in META-IV (the specification language of VDM) towards their refinement into, for example, Pascal or relational DBMSs. The approach includes the automatic synthesis of retrieve functions between models, and data-type invariants.The underlying algebraic semantics is the so-calledfinal semantics à la Wand: a specification is amodel (heterogeneous algebra) which is the final object (up to isomorphism) in the category of all its implementations.The transformational calculus approached in this paper follows from exploring the properties of finite, recursively defined sets.This work extends the well-known strategy of program transformation to model transformation, adding to previous work on a transformational style for operation-decomposition in META-IV. The model-calculus is also useful for improving model-oriented specifications.     

A symbolic approach to automatic multiword term structuring

This paper presents a three-level structuring of multiword terms basing on lexical inclusion, WordNet similarity and a clustering approach. Term clustering by automatic data analysis methods offers an interesting way of organizing a domain’s knowledge structure, useful for several information-oriented tasks like science and technology watch, textmining, computer-assisted ontology population, Question Answering (Q–A). This paper explores how this three-level term structuring brings to light the knowledge structures from a corpus of genomics and compares the mapping of the domain topics against a hand-built ontology (the GENIA ontology). Ways of integrating the results into a Q–A system are discussed.     

A symbolic framework for multi-faceted security protocol analysis

Verification of software systems, and security protocol analysis as a particular case, requires frameworks that are expressive, so as to properly capture the relevant aspects of the system and its properties, formal, so as to be provably correct, and with a computational counterpart, so as to support the (semi-) automated certification of properties. Additionally, security protocols also present hidden assumptions about the context, specific subtleties due to the nature of the problem and sources of complexity that tend to make verification incomplete. We introduce a verification framework that is expressive enough to capture a few relevant aspects of the problem, like symmetric and asymmetric cryptography and multi-session analysis, and to make assumptions explicit, e.g., the hypotheses about the initial sharing of secret keys among honest (and malicious) participants. It features a clear separation between the modeling of the protocol functioning and the properties it is expected to enforce, the former in terms of a calculus, the latter in terms of a logic. This framework is grounded on a formal theory that allows us to prove the correctness of the verification carried out within the fully fledged model. It overcomes incompleteness by performing the analysis at a symbolic level of abstraction, which, moreover, transforms into executable verification tools.     

OFMC: A symbolic model checker for security protocols

We present the on-the-fly model checker OFMC, a tool that combines two ideas for analyzing security protocols based on lazy, demand-driven search. The first is the use of lazy data types as a simple way of building efficient on-the-fly model checkers for protocols with very large, or even infinite, state spaces. The second is the integration of symbolic techniques and optimizations for modeling a lazy Dolev–Yao intruder whose actions are generated in a demand-driven way. We present both techniques, along with optimizations and proofs of correctness and completeness.Our tool is state of the art in terms of both coverage and performance. For example, it finds all known attacks and discovers a new one in a test suite of 38 protocols from the Clark/Jacob library in a few seconds of CPU time for the entire suite. We also give examples demonstrating how our tool scales to, and finds errors in, large industrial-strength protocols.     

A note on commutative multivariate rational series

Direct arguments are presented showing that for rational series in several commuting variables, the rational series problem is undecidable, and closure under Hadamard product fails.     

Unisex: A unix-based symbolic executor for pascal

UNISEX is a UNIX-based symbolic executor for Pascal. The UNISEX system provides an environment for both testing and formally verifying Pascal programs. The system supports a large subset of Pascal, runs on UNIX and provides the user with a variety of debugging features to help in the difficult task of program validation. This paper contains a brief introduction to symbolic execution, followed by an overview of the features of UNISEX, a discussion of the UNISEX Pascal language, and some of the implementation details for the UNISEX system. Finally, some of the problems encountered when designing and implementing the system are discussed as well as future directions.     

A formal methodology for integral security design and verification of network protocols

In this work we propose a methodology for incorporating the verification of the security properties of network protocols as a fundamental component of their design. This methodology can be separated in two main parts: context and requirements analysis along with its informal verification; and formal representation of protocols and the corresponding procedural verification. Although the procedural verification phase does not require any specific tool or approach, automated tools for model checking and/or theorem proving offer a good trade-off between effort and results. In general, any security protocol design methodology should be an iterative process addressing in each step critical contexts of increasing complexity as result of the considered protocol goals and the underlying threats. The effort required for detecting flaws is proportional to the complexity of the critical context under evaluation, and thus our methodology avoids wasting valuable system resources by analyzing simple flaws in the first stages of the design process. In this work we provide a methodology in coherence with the step-by-step goals definition and threat analysis using informal and formal procedures, being our main concern to highlight the adequacy of such a methodology for promoting trust in the accordingly implemented communication protocols. Our proposal is illustrated by its application to three communication protocols: MANA III, WEP's Shared Key Authentication and CHAT-SRP.     

SecDec: A general program for sector decomposition

We present a program for the numerical evaluation of multi-dimensional polynomial parameter integrals. Singularities regulated by dimensional regularisation are extracted using iterated sector decomposition. The program evaluates the coefficients of a Laurent series in the regularisation parameter. It can be applied to multi-loop integrals in Euclidean space as well as other parametric integrals, e.g. phase space integrals.

Program summary

Program title: SecDecCatalogue identifier: AEIR_v1_0Program summary URL:http://cpc.cs.qub.ac.uk/summaries/AEIR_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.: 57 617No. of bytes in distributed program, including test data, etc.: 895 550Distribution format: tar.gzProgramming language: Wolfram Mathematica, perl, FortranComputer: From a single PC to a cluster, depending on the problemOperating system: Unix, LinuxRAM: Depends on the complexity of the problemClassification: 4.4, 5, 11.1Nature of problem: Extraction of ultraviolet and infrared singularities from parametric integrals appearing in higher order perturbative calculations in gauge theories, e.g. multi-loop Feynman integrals, Wilson loops, phase space integrals.Solution method: Algebraic extraction of singularities in dimensional regularisation using iterated sector decomposition. This leads to a Laurent series in the dimensional regularisation parameter ε, where the coefficients are finite integrals over the unit-hypercube. Those integrals are evaluated numerically by Monte Carlo integration.Restrictions: Depending on the complexity of the problem, limited by memory and CPU time. Multi-scale integrals can only be evaluated at Euclidean points.Running time: Between a few minutes and several days, depending on the complexity of the problem.     

A formal approach to object-oriented databases

Object-oriented database systems are the focus of current research and development efforts. Yet, there is no commonly accepted object model, nor is it clear whether such a model can be developed. This paper reports on efforts to develop a formal framework that contains most features found in current object oriented database systems. The framework contains two parts. The first is a structural object model, including concepts such as structured objects, identity, and some form of inheritance. For this model, we explain the distinction between values and (abstract) objects, describe a system as a directed graph, and discuss declarative languages. The second part deals with higher-order concepts, such as classes and functions as data, methods, and inheritance. This part is a sketch, and leaves many issues unresolved. Throughout the paper, the emphasis is on logic-oriented modeling.     

A synergistic approach to improving symbolic execution using test ranges

Innovations in Systems and Software Engineering - Symbolic execution is a systematic technique for checking programs, which has received a lot of research attention during the last decade. In...     

A symbolic model checking approach to verifying satellite onboard software

This paper discusses the use of symbolic model checking technology to verify the design of an embedded satellite software control system called the attitude and orbit control system (AOCS). This system is mission critical because it is responsible for maintaining the attitude of the satellite and for performing fault detection, isolation, and recovery decisions. An executable AOCS implementation by Space Systems Finland has been provided in Ada source code form, and we use the input language of the symbolic model checker NuSMV 2 to model the implementation at a detailed level. We describe the modeling techniques and abstractions used to alleviate the state space explosion due to the handling of timers and the large number of system components controlled by the AOCS. The required behavior has been specified as extended state machine diagrams and translated to temporal logic properties. Besides well-known LTL and CTL model checking algorithms, we adapt a previously unexplored form of the liveness-to-safety approach to the problem. The latter new technique turns out to successfully prove all desired properties of the system, outperforming both the LTL and CTL implementations of NuSMV 2.