The Isabelle/HOL proof assistant provides quite advanced and reliable support for discharging proof goals with external SMT solvers by reconstructing the resulting proof tree within the Isabelle/Pure inference kernel....
详细信息
ISBN:
(数字)9781665412919
ISBN:
(纸本)9781665448215
The Isabelle/HOL proof assistant provides quite advanced and reliable support for discharging proof goals with external SMT solvers by reconstructing the resulting proof tree within the Isabelle/Pure inference kernel. In particular, currently Isabelle fully and efficiently supports proof reconstruction for the quantifier-free fragments of the theories of equality and uninterpreted functions (QF_UF) and linear integer arithmetic (QF_LIA). Yet there are a number of practically relevant theories that can be decided using relatively efficient algorithms, but are not supported either by the Isabelle proof reconstruction procedure or by the SMT solvers themselves. Meanwhile, if the decision procedure for an extended logical theory can be expressed as a complete quantifier instantiation strategy that reduces the given decision problem into the supported logical fragment (QF_UFLIA), the theory can be fully supported within the existing Isabelle/HOL infrastructure with relatively little additional effort. The goal of our work was to develop a fully formal completeness proof for an efficient quantifier instantiation strategy that translates a satisfiability problem in the logic of bounded linear integer arithmetic (we call it QF_BLIA) into the equisatisfiable problem in the logic of linear integer arithmetic and uninterpreted functions (QF_UFLIA). In this paper we first give the initial informal presentation of the proof, then discuss the most relevant issues of our resulting corresponding formal development of the completeness proof within Isabelle/HOL. The resulting formal proofs tightly follow the provided informal presentation, but at the same time they also contain quite significant amount of auxiliary developments that can potentially be generalized for other similar proof formalizations and automated using theory generation facilities of Isabelle/ML.
Recently, Fuzzing is one of the most successful techniques to expose bugs in software. For testing large programs or large codebase with many features and entry-points, the creation of fuzz-targets remains a big chall...
详细信息
ISBN:
(纸本)9781665423281
Recently, Fuzzing is one of the most successful techniques to expose bugs in software. For testing large programs or large codebase with many features and entry-points, the creation of fuzz-targets remains a big challenge. In this paper, we introduce Futag – an automated fuzz target generator for testing software libraries. This approach uses static analysis to collect information about source code: data type definitions, dependencies of types, definitions of functions, etc. Futag has found many vulnerabilities in latest version of popular libraries such as: libopenssl, libpng, libjson-c, liblxml2.
The computer industry and the science of computer science that emerged in the Soviet Union in the late 1940s, constantly evolving and continuously transforming, went through several stages in its innovative developmen...
详细信息
ISBN:
(纸本)9781728112763;9781728112756
The computer industry and the science of computer science that emerged in the Soviet Union in the late 1940s, constantly evolving and continuously transforming, went through several stages in its innovative development. The article is devoted to the history of the formation of Russian computer science. One of the stages of the continuous innovation development of computer science in Russia is connected with the intensive development of new directions in system and applied programming, to which the reports presented at the conference are devoted.
In this paper, we consider checking the robustness of web services using the model of finite state automata and analyzing the solvability of an automaton equation over the concatenation operator. The paper contains th...
详细信息
The article outlines the basic design principles of the Electronica SS BIS software and computing complex, aimed at addressing the most complex scientific problems. The developers have researched heterogeneous computi...
详细信息
ISBN:
(数字)9798331504663
ISBN:
(纸本)9798331504670
The article outlines the basic design principles of the Electronica SS BIS software and computing complex, aimed at addressing the most complex scientific problems. The developers have researched heterogeneous computing supersystems due to the experience they had accumulated from creating previous systems. Research has shown that integrating closely related subsystems with different architectures results in more effective computing systems. With this approach, supercomputers not only became multiprocessors, but they also combined a number of subsystems or independent functional systems, such as a multi-level memory system, a system of functionally specialized machines, a channel system, and a distributed operating system. Later, this work became the foundation for a new direction in computing technology—computing supersystems. In recent years this direction has been recognized as highly relevant and promising.
Dynamic symbolic execution is a widely used technique for automated software testing, designed for execution paths exploration and program errors detection. A hybrid approach has recently become widespread, when the m...
详细信息
ISBN:
(纸本)9781665423281
Dynamic symbolic execution is a widely used technique for automated software testing, designed for execution paths exploration and program errors detection. A hybrid approach has recently become widespread, when the main goal of symbolic execution is helping fuzzer increase program coverage. The more branches symbolic executor can invert, the more useful it is for fuzzer. A program control flow often depends on memory values, which are obtained by computing address indexes from user input. However, most DSE tools don’t support such dependencies, so they miss some desired program *** implement symbolic addresses reasoning on memory reads in our dynamic symbolic execution tool Sydr. Possible memory access regions are determined by either analyzing memory address symbolic expressions, or binary searching with SMT-solver. We propose an enhanced linearization technique to model memory *** memory modeling methods are compared on the set of programs. Our evaluation shows that symbolic addresses handling allows to discover new symbolic branches and increase the program coverage.
Reputation and competitiveness of both mobile applications and mobile operating systems depend on their quality. Developers are using various techniques to ensure high quality. Recently, exploratory testing approaches...
详细信息
Reputation and competitiveness of both mobile applications and mobile operating systems depend on their quality. Developers are using various techniques to ensure high quality. Recently, exploratory testing approaches have been gaining significant attention in this context. However, these approaches mostly do not consider one major non-functional requirement that affects quality – performance issues. Performance issues, such as sluggish UI or extensive battery consumption, are tightly connected to inefficient use of device resources. Detecting these issues is a non-trivial task. In this paper we present a novel approach to detect anomalous device resource usage and hence potential performance issues. Our approach is integrated with exploratory testing framework and uses information about previously executed test runs to build the expected resource usage model. The underlying model represents resource usage data as a multidimensional time series and is able to detect anomalous time intervals. We integrate our approach with exploratory testing tool for Android and empirically evaluate it on a set of real-world applications with injected performance issues. Our results show that suggested approach can be successfully applied to detect anomalous device resource usage and potential performance regressions.
This paper considers open-source tools for the logical-synthesis and place-and-route hardware design stages. Several flows (CADs), including qFlow, OpenLANE, Coriolis, VTR, and SymbiFlow, have been described. For expe...
详细信息
This paper presents a calculation of the aerodynamic characteristics of the ZOHD Alpha Strike UAV model, designed with a delta wing. The focus of the study is the overall layout of the aircraft and the influence of th...
This paper presents a calculation of the aerodynamic characteristics of the ZOHD Alpha Strike UAV model, designed with a delta wing. The focus of the study is the overall layout of the aircraft and the influence of the propeller on its aerodynamic characteristics. The computational fluid dynamics tool OpenFOAM is used as an effective method to solve the complex aerodynamic problems inherent in this UAV model. Research is carried out in an incompressible flow, due to the low speeds inherent in such aircraft. A numerical methodology is proposed for quick evaluation of the aerodynamic performances of UAV models with a propeller. A simple dynamic model and flight data are presented. The calculation results are verified using a flight experiment.
Dynamic symbolic execution is a widely used technique for automated software testing, designed for execution paths exploration and program errors detection. A hybrid approach has recently become widespread, when the m...
详细信息
暂无评论