作者:
Colón, MAUSN
Res Lab Ctr High Assurance Comp Syst Washington DC 20375 USA
We present a method for schema-guided synthesis of imperative programs computing polynomial functions and their inverses. the schemas of our approach contain parameters representing both fragments of code and fragment...
详细信息
ISBN:
(纸本)3540266550
We present a method for schema-guided synthesis of imperative programs computing polynomial functions and their inverses. the schemas of our approach contain parameters representing both fragments of code and fragments of invariants, and they generate programs annotated with loop invariants establishing partial correctness. Schema application entails simultaneously instantiating the code parameters to polynomials and the invariant parameters to systems of polynomial equalities. By bounding the degrees of these polynomials and their number, our method reduces schema instantiation to non-linear constraint solving, based on the theory of polynomial ideals. Although non-linear constraint solving is NP-hard, a solution can be generated automatically when the. resulting system contains few constraints. A specialization of our method yields linear constraints by further restricting the form of the invariants. this restriction improves the efficiency of constraint solving, but may fail to synthesize programs derivable by the general method.
In this paper, we present a fast binding-time analysis (BTA) by integrating a size-change analysis, which is independent of a selection rule, into a classical BTA for offline partial evaluation of logicprograms. In c...
详细信息
ISBN:
(纸本)9783642005145
In this paper, we present a fast binding-time analysis (BTA) by integrating a size-change analysis, which is independent of a selection rule, into a classical BTA for offline partial evaluation of logicprograms. In contrast to previous approaches, the new BTA is conceptually simpler and considerably faster, scaling to medium-sized or even large examples and, moreover, it ensures boththe so called local and global termination. We also show that;through the use of selective hints, we call achieve both good specialisation results and a fast BTA and specialisation process.
this book constitutes the thoroughly refereed post-conference proceedings of the 29thinternationalsymposium on logic-basedprogramsynthesis and transformation, LOPSTR 2019, held in Porto, Portugal, in October 2019....
详细信息
ISBN:
(数字)9783030452605
ISBN:
(纸本)9783030452599
this book constitutes the thoroughly refereed post-conference proceedings of the 29thinternationalsymposium on logic-basedprogramsynthesis and transformation, LOPSTR 2019, held in Porto, Portugal, in October 2019. the 15 revised full papers were carefully reviewed and selected from 32 submissions. In addition to the 15 papers, this volume includes 2 invited papers.;the symposium cover all aspects of logic-basedprogram development, stages of the software life cycle, and issues of bothprogramming-in-the-small and programming-in-the-large. this year LOPSTR extends its traditional topics to include also logic-basedprogram development based on integration of sub-symbolic and symbolic models, on machine learning techniques and on differential semantics. the papers are grouped into the following topics: static analysis, programsynthesis, constraints and unification, debugging and verification, and programtransformation.
Visualization tools of different languages offer its users with a needed set of features allowing them to animate how programs of such languages work. Constraint Handling Rules (CHR) is currently used as a general pur...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
Visualization tools of different languages offer its users with a needed set of features allowing them to animate how programs of such languages work. Constraint Handling Rules (CHR) is currently used as a general purpose language. this results in having complex programs with CHR. Nevertheless, CHR is still lacking on visualization tools. With Constraint Handling Rules (CHR) being a high-level rule-based language, animating CHR programs through animation tools demonstrates the power of the language. Such tools are useful for beginners to the language as well as programmers of sophisticated algorithms. this paper continues upon the efforts made to have a generic visualization platform for CHR using source-to-source transformation. It also provides a new visualization feature that enables viewing all the possible solutions of a CHR program instead of the don't care nondeterminism used in most CHR implementations.
A nonvolatile FPGA, where the circuit-configuration information still remains without power supply, offers a powerful solution against the standby power issue. In this paper, a synthesizable nonvolatile FPGA is propos...
详细信息
ISBN:
(纸本)9781728154060
A nonvolatile FPGA, where the circuit-configuration information still remains without power supply, offers a powerful solution against the standby power issue. In this paper, a synthesizable nonvolatile FPGA is proposed, where the circuit-configuration information is described in a hardware description language and is pushed through a standard ASIC tool flow with nonvolatile logic circuit IPs such as nonvolatile flip-flops. the use of the ASIC tool flow makes it possible to migrate any arbitrary process technology and to perform architecture-level simulation with physical information. As a typical design example under 55nm CMOS/100nm magnetic tunnel junction (MTJ) technologies, the performance of the proposed nonvolatile FPGA is evaluated in comparison withthat of a CMOS-only volatile FPGA.
programsynthesis offers an attractive alternative to the intricate and tedious process of writing assembly programs manually. Assembly programsynthesis automatically generates implementations, given a high-level for...
详细信息
ISBN:
(纸本)9783031712937;9783031712944
programsynthesis offers an attractive alternative to the intricate and tedious process of writing assembly programs manually. Assembly programsynthesis automatically generates implementations, given a high-level formal specification and a machine description. However, its limited scalability prevents widespread adoption. Automatic parallelization improves programsynthesis in general, but parallelizing assembly synthesis is nontrivial as the realities that data are untyped and all state is global lead to an enormous search space and prevent straightforward decomposition into separable sub-problems that can be run in parallel. We present PASSES, a Parallel Assembly synthesis System Exploiting Subspaces. PASSES uses five heuristics to transform an original assembly synthesis problem into a set of sub-problems;it runs multiple synthesis sub-problems in parallel and constructs the final result by combining them. We evaluate PASSES on 26 general bit manipulation assembly programming problems and 140 machine-dependent use cases from two operating systems. Compared to an existing assembly synthesis tool and a state-of-the-art parallel SMT solver, all five heuristics in PASSES significantly improve assembly synthesis scalability.
the goal of automated programsynthesis is to bridge the gap between what is easy for people to describe and what is possible to execute on a computer. In this paper, we present a framework for synthesis of rule-based...
ISBN:
(纸本)3540404384
the goal of automated programsynthesis is to bridge the gap between what is easy for people to describe and what is possible to execute on a computer. In this paper, we present a framework for synthesis of rule-based solvers for constraints given their logical specification. this approach takes advantage of the power of tabled resolution for constraint logicprogramming, in order to check the validity of the rules. Compared to previous work [8,19,2,5,3], where different methods for automatic generation of constraint solvers have been proposed, our approach enables the generation of more expressive rules (even recursive and splitting rules).
A pattern t, i.e., a term possibly with variables, denotes the set (language) [t] of all its ground instances. In an untyped setting, symbolic operations on finite sets of patterns can represent Boolean operations on ...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
A pattern t, i.e., a term possibly with variables, denotes the set (language) [t] of all its ground instances. In an untyped setting, symbolic operations on finite sets of patterns can represent Boolean operations on languages. But for the more expressive patterns needed in declarative languages supporting rich type disciplines such as subtype polymorphism untyped pattern operations and algorithms break down. We show how they can be properly defined by means of a signature transformation Sigma bar right arrow Sigma(#) that enriches the types of S. We also show that this transformation allows a systematic reduction of the first-order logic properties of an initial order-sorted algebra supporting subtype-polymorphic functions to equivalent properties of an initial many-sorted (i.e., simply typed) algebra. this yields a new, simple proof of the known decidability of the first-order theory of an initial order-sorted algebra.
We address the problem of the automated verification of temporal properties of infinite state reactive systems. We present some improvements of a verification method based on the specialization of constraint logic pro...
详细信息
ISBN:
(纸本)9783642205507
We address the problem of the automated verification of temporal properties of infinite state reactive systems. We present some improvements of a verification method based on the specialization of constraint logicprograms (CLP). First, we reformulate the verification method as a two-phase procedure: (1) in the first phase a CLP specification of an infinite state system is specialized with respect to the initial state of the system and the temporal property to be verified, and (2) in the second phase the specialized program is evaluated by using a bottom-up strategy. In this paper we propose some new strategies for performing program specialization during the first phase. We evaluate the effectiveness of these new strategies, as well as that of some old strategies, by presenting the results of experiments performed on several infinite state systems and temporal properties. Finally, we compare the implementation of our specialization-based verification method with various constraint-based model checking tools. the experimental results show that our method is effective and competitive with respect to the methods used in those other tools.
Round-off errors arising from the difference between real numbers and their floating-point representation cause the control flow of conditional floating-point statements to deviate from the ideal flow of the real-numb...
详细信息
ISBN:
(纸本)9783030138387;9783030138370
Round-off errors arising from the difference between real numbers and their floating-point representation cause the control flow of conditional floating-point statements to deviate from the ideal flow of the real-number computation. this problem, which is called test instability, may result in a significant difference between the computation of a floating-point program and the expected output in real arithmetic. In this paper, a formally proven programtransformation is proposed to detect and correct the effects of unstable tests. the output of this transformation is a floating-point programthat is guaranteed to return either the result of the original floating-point program when it can be assured that both its real and its floating-point flows agree or a warning when these flows may diverge. the proposed approach is illustrated withthe transformation of the core computation of a polygon containment algorithm developed at NASA that is used in a geofencing system for unmanned aircraft systems.
暂无评论