Concolic execution, a combination of concrete and symbolic execution, has become increasingly popular in recent approaches to model checking and test case generation. In general, an interpreter of the language is augm...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
Concolic execution, a combination of concrete and symbolic execution, has become increasingly popular in recent approaches to model checking and test case generation. In general, an interpreter of the language is augmented in order to also deal with symbolic values. In this paper, in contrast, we present an alternative approach that is based on a program instrumentation. Basically, the execution of the instrumented program in a standard environment produces a sequence of events that can be used to reconstruct the associated symbolic execution.
this work is inspired by D.R. Smith’s research on synthesising global search (GS) programs (in the Refine language) from first-order logic specifications (also in Refine) [8,9,10]. We concentrate on synthesi...
ISBN:
(数字)9783540489580
ISBN:
(纸本)3540657657
this work is inspired by D.R. Smith’s research on synthesising global search (GS) programs (in the Refine language) from first-order logic specifications (also in Refine) [8,9,10]. We concentrate on synthesising constraint logicprograms (CLP) [6] instead. We thus only have to synthesise code that (incrementally) poses the constraints, because the actual constraint propagation and pruning are performed by the CLP system. We here only tackle the family of decision assignment problems; the families of optimisation assignment problems, decision permutation problems, and optimisation permutation problems are covered in [4].
作者:
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.
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.
In this paper, we develop a bottom-up fixed point semantics for pure Prolog programs extended with !/0 that allows to reconstruct the operational semantics of a particular goal. Our semantics captures boththe order i...
ISBN:
(纸本)3540404384
In this paper, we develop a bottom-up fixed point semantics for pure Prolog programs extended with !/0 that allows to reconstruct the operational semantics of a particular goal. Our semantics captures boththe order in which solutions are computed by SLD-resolution and their multiplicity.
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.
Static type systems are usually not sufficient to express all requirements on function calls. Hence, contracts with pre-and postconditions can be used to express more complex constraints on operations. Contracts can b...
详细信息
ISBN:
(纸本)9783319944609;9783319944593
Static type systems are usually not sufficient to express all requirements on function calls. Hence, contracts with pre-and postconditions can be used to express more complex constraints on operations. Contracts can be checked at run time to ensure that operations are only invoked with reasonable arguments and return intended results. Although such dynamic contract checking provides more reliable program execution, it requires execution time and could lead to program crashes that might be detected with more advanced methods at compile time. To improve this situation for declarative languages, we present an approach to combine static and dynamic contract checking for the functional logic language Curry. based on a formal model of contract checking for functional logicprogramming, we propose an automatic method to verify contracts at compile time. If a contract is successfully verified, dynamic checking of it can be omitted. this method decreases execution time without degrading reliable program execution. In the best case, when all contracts are statically verified, it provides trust in the software since crashes due to contract violations cannot occur during program execution.
the proceedings contain 18 papers. the special focus in this conference is on logicprogramsynthesis and transformation. the topics include: Refining specifications to logicprograms;symbolic verification with gap-or...
ISBN:
(纸本)3540627189
the proceedings contain 18 papers. the special focus in this conference is on logicprogramsynthesis and transformation. the topics include: Refining specifications to logicprograms;symbolic verification with gap-order constraints;specification-based automatic verification of prolog programs;logicprogram specialisation;conjunctive partial deduction in practice;redundant argument filtering of logicprograms;replacement can preserve termination;a transformation tool for pure prolog programs;enhancing partial deduction via unfold/fold rules;abstract specialization and its application to program parallelization;reductions of petri nets and unfolding of propositional logicprograms;inferring argument size relationships with CLP(R);typed norms for typed logicprograms;partial deduction in the framework of structural synthesis of programs;extensible logicprogram schematar;specialising meta-level compositions of logicprograms;forms of logic specifications;synthesis of proof procedures for default reasoning.
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.
暂无评论