program slicing has been mainly studied in the context of imperative languages, where it has been applied to a wide variety of software engineering tasks, like program understanding, maintenance, debugging, testing, c...
详细信息
the proceedings contain 14 papers. the special focus in this conference is on programtransformation, Equivalence, program Verificaion and program Analysis. the topics include: Static analysis for safe destructive upd...
ISBN:
(纸本)3540439153
the proceedings contain 14 papers. the special focus in this conference is on programtransformation, Equivalence, program Verificaion and program Analysis. the topics include: Static analysis for safe destructive updates in a functional language;a transformation technique for datalog programs based on non-deterministic constructs;on deforesting parameters of accumulating maps;abstract conjunctive partial deduction using regular types and its application to model checking;verification of sets of infinite state processes using programtransformation;symbolic profiling for multi-paradigm declarative languages;correct object-oriented systems in computational logic;a framework for developing embeddable customized logics;extracting general recursive program schemes in nuprl’s type theory and extracting exact time bounds from logical proofs.
the proceedings contains 11 papers. the topics discussed include: declarative programming with function patterns;transformational verification of parameterized protocols using array formulas;an algorithm for local var...
详细信息
ISBN:
(纸本)3540326545
the proceedings contains 11 papers. the topics discussed include: declarative programming with function patterns;transformational verification of parameterized protocols using array formulas;an algorithm for local variable elimination normal logicprograms;removing superfluous versions in polyvariant specialization of prolog programs;extension of type-based approach to generation of stream-processing programs by automatic insertion of buffering primitives;non-leftmost unfolding in partial evaluation of logicprograms with impure predicates;a transformational semantics of static embedded implications of normal logicprograms;converting one type-based abstract domain to another;and experiments in context-sensitive analysis of modular programs.
作者:
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.
To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. this process is particularly effective i...
详细信息
the proceedings contain 22 papers. the special focus in this conference is on Debugging and types, Tabling and constraints, Abstract interpretation, program refinement, Verification, Partial evaluation and Rewriting a...
ISBN:
(纸本)9783540404385
the proceedings contain 22 papers. the special focus in this conference is on Debugging and types, Tabling and constraints, Abstract interpretation, program refinement, Verification, Partial evaluation and Rewriting and object-oriented development. the topics include: Abstract diagnosis of functional programs;a cut-free sequent calculus for pure type systems verifying the structural rules of gentzen/kleene;constraint solver synthesis using tabled resolution for constraint logicprogramming;translating datalog-like optimization queries into ILOG programs;tabling structures for bottom-up logicprogramming;towards optimal operators for sharing properties;two variables per linear inequality as an abstract domain;convex hull abstractions in specialization of CLP programs;collecting potential optimisations;an operational approach to program extraction in the calculus of constructions;refinement of higher-order logicprograms;a generic program for minimal subsets with applications;justification based on programtransformation;combining logicprograms and monadic second order logics by programtransformation;verification in ACL2 of a generic framework to synthesize SAT-provers;a proof system for information flow security;forward slicing of multi-paradigm declarative programs based on partial evaluation;a fixed point semantics for logicprograms extended with cuts;abstract partial deduction challenged;towards correct object-oriented design frameworks in computational logic;mapping modular SOS to rewriting logic and programsynthesisbased on the equivalent transformation computation model.
the proceedings contain 14 papers. the topics discussed include: a transformation technique for datalog programs based on non-deterministic constructs;on deforesting parameters of accumulating maps;equivalence in answ...
ISBN:
(纸本)3540439153
the proceedings contain 14 papers. the topics discussed include: a transformation technique for datalog programs based on non-deterministic constructs;on deforesting parameters of accumulating maps;equivalence in answer set programming;extracting exact time bounds from logical proofs;extracting general recursive program schemes in Nuprl's type theory;computing environment-aware agent behaviors withlogicprogram updates;a framework for developing embeddable customized logics;correct object-oriented systems in computational logic;symbolic profiling for multi-paradigm declarative languages;when size does matter;verification of sets of infinite state processes using programtransformation;and abstract conjunctive partial deduction using regular types and its application to model checking.
Effective generation of efficient and correct programs from specifications is the underlying design motivation of the Equivalent transformation (ET) computation model. this concise paper explains how the ET model sati...
ISBN:
(纸本)3540404384
Effective generation of efficient and correct programs from specifications is the underlying design motivation of the Equivalent transformation (ET) computation model. this concise paper explains how the ET model satisfies major required features of a programsynthesis framework, and outlines a three-phase programsynthesis method.
We present a programsynthesis method based on unfold/fold transformation rules which can be used for deriving terminating definite logicprograms from formulas of the Weak Monadic Second Order theory of one successor...
ISBN:
(纸本)3540404384
We present a programsynthesis method based on unfold/fold transformation rules which can be used for deriving terminating definite logicprograms from formulas of the Weak Monadic Second Order theory of one successor (WS1S). this synthesis method can also be used as a proof method which is a decision procedure for closed formulas of WS1S. We apply our synthesis method for translating CLP(WS1S) programs into logicprograms and we use it also as a proof method for verifying safety properties of infinite state systems.
A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we extend the refinement calculus fo...
ISBN:
(纸本)3540404384
A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we extend the refinement calculus for logicprograms to include higher-order programming capabilities in specifications and programs, such as procedures as terms and lambda abstraction. We use a higher-order type and term system to describe programs, and provide a semantics for the higher-order language and refinement. the calculus is illustrated by refinement examples.
暂无评论