1,720,996 research outputs found
WSSMT: Towards the Automated Analysis of Security-Sensitive Services and Applications
No full textThe security of service-oriented applications is crucial in several contexts such as e-commerce or e-governance. The design, implementation, and deployment of this kind of services are often so complex that serious vulnerabilities remain even after extensive application of traditional validation techniques, such as testing. Given the importance of security-sensitive service applications, the development of techniques for their automated validation is growing. In this paper, we illustrate our formal framework to the specification and validation of security-sensitive applications structured in two levels: the workflow level (dealing with the control of flow and the manipulation of data) and the policy level (describing trust relationships and access control). In our framework, verification problems are reduced to logical problems whose decidability can be shown under suitable assumptions, which permit the validation of practically relevant classes of services. As a by-product, it is possible to re-use state-of-the-art theorem-proving technology to mechanize the verification process. This is the idea underlying our prototype validation tool WSSMT, "Web-Service (validation by) Satisfiability Modulo Theories'', which has been successfully used on two industrial case studies taken from the FP7 European project AVANTSSAR
An Algorithm for Exact Division
No full textAbstractCurrent computer algebra systems use the quotient-remainder algorithm for division of long integers even when it is known in advance that the remainder is zero. We propose an algorithm which computes the quotient of two long integers in this particular situation, starting from the least-significant digits of the operands. This algorithm is particularly efficient when the radix is a prime number or a power of 2.The computing time of this new algorithm is smaller than the computing time of the classical division algorithm. If the length of the result is much smaller than the lengths of the inputs, then the speed-up may be quite significant, as it is confirmed by practical experiments.Most importantly, however, the new algorithm is better suited for systolic parallelization in a "least-significant digit first" pipelined manner, and therefore it is suitable for aggregation with other systolic algorithms for the arithmetic of long integers and long rationals.We also present applications of this algorithm in integer GCD computation and in division modulo a power of 2
A heuristic prover for elementary analysis in theorema : RISC Report Series, 21-07
No full textWe present the application of certain heuristic techniques for the automation of proofs in elementary analysis. the techniques used are: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the [Epsilon]-bounds, semantic simplification of expressions involving absolute value, polynomial arithmetic, usage of equal arguments to arbitrary functions, and automatic reordering of proof steps in order to check the admisibility of solutions to the metavariables. The proofs are very similar to those produced automatically, but they are edited for readability and aspect, and also for inserting the appropriate explanation about the use of the proof techniques. The proofs are: convergence of product of two sequences, continuity of the sum of two functions, uniform continuity of the sum of two functions, uniform continuity of the product of two functions!, and continuity of the composition of functions
A Double-Digit Lehmer-Euclid Algorithm for Finding the GCD of Long Integers
No full textAbstractThe use of pairs of double digits in the Lehmer-Euclid multiprecision GCD algorithm halves the number of long multiplications, but a straightforward implementation of this idea does not give the desired speed-up. We show how to overcome the practical difficulties by using an enhanced condition for exiting the partial cosequence computation. Also, additional speed-up is achieved by approximative GCD computation. The combined effect of these improvements is an experimentally measured speed-up by a factor of 2 for operands with 100 32-bit words
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Preface Volume 23, Issue 3
No full textAbstractThis volume contains the Proceedings of Calculemus 99, a satellite workshop of CADE 16: “Computer Aided Deduction”, itself a part of FLoC 99: “Federated Logic Conference”.The workshop addressed the problem of combining the reasoning capabilities of Deduction Systems and the computational power of Computer Algebra Systems. This topic is of particular interest since both Deduction Systems and Computer Algebra Systems are receiving growing attention from industry and academia. On the one hand, Mathematical Software Systems have been commercially very successful: their use is now wide-spread in industry, education, and in scientific contexts. On the other hand, the use of formal methods in hardware and software development makes Deduction Systems indispensable not least because of the complexity and sheer size of the reasoning tasks involved. In spite of these successes there is still need for improvement as many application domains still fall outside the scope of existing Deduction Systems and Computer Algebra Systems. The emphasis of the workshop was on whether existing systems and technologies can be integrated as they stand or if a fundamental redesign is necessary.The proceedings contain contributions from some of the most important scientific groups involved in research and applications of automatic deduction and symbolic computation. The 11 papers selected by the programme committee and the two invited talks address various aspects related to the combination of deduction systems and computer algebra systems, including case studies and results from applications.
We express special thanks to the Program Committee members:Alessandro Armando (Co-Chair)(University of Genova & LORIA-INRIA-Lorraine)Henk Barendregt(University of Nijmegen)Bruno Buchberger(RISC-Linz)Alan Bundy(University of Edinburgh)Jaques Calmet(University of Karlsruhe)Edmund Clarke(Carnegie Mellon University)Bernd Ingo Dahn(University of Koblenz-Landau)Fausto Giunchiglia(IRST, Trento and University of Trento)Hoon Hong(University of North Carolina)Tetsuo Ida(Tsukuba University)Tudor Jebelean (Co-Chair)(RISC-Linz)Manfred Kerber(University of Birmingham)Michael Kohlhase(University of Saarbrücken)Alexander Letichevsky(Glushkov Institute of Cybernetics, Kiev)Ursula Martin(St. Andrews University)Lawrence C. Paulson(University of Cambridge)Joerg Siekmann(University of Saarbrücken)Carolyn Talcott(Stanford University)Andrzej Trybulec(University of Bialystok)Dongming Wang(IMAG Grenoble)We also whish to thank the following people, who - together with the programme committee - helped us in the reviewing process: Alessandro Coglio (Kestrel Institute, USA), Katherine Eastaughffe (University of Cambridge), Andrew Ireland (Heriot-Watt University), Boris Konev (Steklov Institute of Mathematics, St. Petersburg), Silvio Ranise (University of Genova), and Klaus Sutner (Carnegie Mellon University).The organizers of FLoC 99 gave us valuable help in the local organization during the Workshop. We also thank Michael Mislove, Managing Editor of the Electronic Notes in Computer Science series for giving us the opportunity of publishing the proceedings this new series, and for the support he provided us during the preparation of this volume.Alessandro Armando and Tudor Jebelean, Guest Editor
Variations on the Author
Full text link“Variations on the Author” discusses two of Eduardo Coutinho’s recent films (Um Dia na Vida, from 2010, and Últimas Conversas, posthumously released in 2015) and their contribution to the general question of documentary authorship. The director’s filmography is characterized by a consistent yet self-effacing form of authorial self-inscription: Coutinho often features as an interviewer that rather than express opinions propels discourses; an interviewer that is good at listening. This mode of self-inscription characterizes him as an author who is not expressive but who is nonetheless markedly present on the screen. In Um Dia na Vida, however, Coutinho is completely absent form the image, while Últimas Conversas, on the contrary, includes a confessional prologue that moves the director from the margins to the center of his films. This article examines the ways in which these works stand out in the filmography of a director who offers new insights into the notion of cinematic authorship
Appropriate Similarity Measures for Author Cocitation Analysis
Full text linkWe provide a number of new insights into the methodological discussion about author cocitation analysis. We first argue that the use of the Pearson correlation for measuring the similarity between authors’ cocitation profiles is not very satisfactory. We then discuss what kind of similarity measures may be used as an alternative to the Pearson correlation. We consider three similarity measures in particular. One is the well-known cosine. The other two similarity measures have not been used before in the bibliometric literature. Finally, we show by means of an example that our findings have a high practical relevance.information science;Pearson correlation;cosine;similarity measure;author cocitation analysis
Solving Robust Glucose-Insulin Control by Dixon Resultant Computations
Full text linkWe present a symbolic approach towards solving the Bergman three-state minimal patient model of glucose metabolism. Our work first translates the Bergman three-state minimal patient model into the modified control algebraic Riccati equation. Next, the modified control algebraic Ricatti equation is reduced to a system of polynomial equations, and an optimal (minimal) solution of these polynomials is computed using Dixon resultants. We demonstrate the use of our method by reporting on three case studies over glucose metabolism
- …
