this work presents a static analysis technique based on program slicing for CSP specifications. Given a particular event in a CSP specification, our technique allows us to know what parts of the specification must nec...
详细信息
ISBN:
(纸本)9783642005145
this work presents a static analysis technique based on program slicing for CSP specifications. Given a particular event in a CSP specification, our technique allows us to know what parts of the specification must necessarily be executed before this event, and what parts of the specification could be executed before it in some execution. Our technique is based on a new data structure which extends the Synchronized Control Flow Graph (SCFG). We show that this new data structure improves the SCFG by taking into account the context in which processes are called and, thus, makes the slicing process more precise.
the proceedings contain 49 papers. the topics discussed include: validity checking of putback transformations in bidirectional programming;a refinement based strategy for local deadlock analysis of networks of CSP pro...
ISBN:
(纸本)9783319064093
the proceedings contain 49 papers. the topics discussed include: validity checking of putback transformations in bidirectional programming;a refinement based strategy for local deadlock analysis of networks of CSP processes;TrustFound: towards a formal foundation for model checking trusted computing platforms;a simplified Z semantics for presentation interaction models;quiescent consistency: defining and verifying relaxed linearizability;temporal precedence checking for switched models and its application to a parallel landing protocol;precise predictive analysis for discovering communication deadlocks in MPI programs;efficient runtime monitoring with metric temporal logic: a case study in the android operating system;checking liveness properties of Presburger counter systems using reachability analysis;co-induction simply: automatic co-inductive proofs in a program verifier;and compositional synthesis of concurrent systems through causal model checking and learning.
the well-founded semantics of normal logicprograms has two main utilities, one being an efficiently computable semantics with a unique intended model, and the other serving as polynomial time constraint propagation f...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
the well-founded semantics of normal logicprograms has two main utilities, one being an efficiently computable semantics with a unique intended model, and the other serving as polynomial time constraint propagation for the computation of answer sets of the same program. When logicprograms are generalized to support constraints of various kinds, the semantics is no longer tractable, which makes the second utility doubtful. this paper considers the possibility of tractable but incomplete methods, which in general may miss information in the computed result, but never generates wrong conclusions. For this goal, we first formulate a well-founded semantics for logicprograms with generalized atoms, which generalizes logicprograms with arbitrary aggregates/constraints/dl-atoms. As a case study, we show that the method of removing non-monotone dl-atoms for the well-founded semantics by Eiter et al. actually falls into this category. We also present a case study for logicprograms with standard aggregates.
Algorithmic debugging is a semi-automatic debugging technique that is present in practically all mature programming languages. In this paper we claim that the state of the practice in algorithmic debugging is a step f...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
Algorithmic debugging is a semi-automatic debugging technique that is present in practically all mature programming languages. In this paper we claim that the state of the practice in algorithmic debugging is a step forward compared to the state of the theory. In particular, we argue that novel techniques for algorithmic debugging cannot be supported by the standard internal data structures used in this technique, and a generalization of the standard definitions and algorithms is needed. We identify two specific problems of the standard formulation and implementations of algorithmic debugging, and we propose a reformulation to solve both problems. the reformulation has been done in a paradigm-independent manner to make it useful and reusable in different programming languages.
the proceedings contain 11 papers. the topics discussed include: space invading systems code;test data generation of bytecode by CLP partial evaluation;a modular equational generalization algorithm;a transformational ...
the proceedings contain 11 papers. the topics discussed include: space invading systems code;test data generation of bytecode by CLP partial evaluation;a modular equational generalization algorithm;a transformational approach to polyvariant BTA of higher-order functional programs;analysis of linear hybrid systems in CLP;automatic generation of test inputs for mercury;analytical inductive functional programming;the MEB and CEB static analysis for CSP specifications;fast offline partial evaluation of large logicprograms;an inference algorithm for guaranteeing safe destruction;from monomorphic to polymorphic well-typings and beyond;and on negative unfolding in the answer set semantics.
A major impediment for more widespread use of offline partial evaluation is the difficulty of obtaining and maintaining annotations for larger, realistic programs. Existing automatic binding-time analyses still only h...
详细信息
ISBN:
(纸本)9783540714095
A major impediment for more widespread use of offline partial evaluation is the difficulty of obtaining and maintaining annotations for larger, realistic programs. Existing automatic binding-time analyses still only have limited applicability and annotations often have to be created or improved and maintained by hand, leading to errors. We present a technique to help overcome this problem by using online control techniques which supervise the specialisation process in order to detect such errors. We discuss an implementation in the LOGEN system and show on a series of examples that this approach is effective: very few false alarms were raised while infinite loops were detected quickly. We also present the integration of this technique into a web interface, which highlights problematic annotations directly in the source code. A method to automatically fix incorrect annotations is presented, allowing the approach to be also used as a pragmatic binding time analysis. Finally we show how our method can be used for efficiently locating errors with built-ins inside Prolog source code.
this book constitutes the thoroughly refereed post-conference proceedings of the 28thinternationalsymposium on logic-basedprogramsynthesis and transformation, LOPSTR 2018, held in Frankfurt/Main, Germany, in Septe...
详细信息
ISBN:
(数字)9783030138387
ISBN:
(纸本)9783030138370
this book constitutes the thoroughly refereed post-conference proceedings of the 28thinternationalsymposium on logic-basedprogramsynthesis and transformation, LOPSTR 2018, held in Frankfurt/Main, Germany, in September 2018.;the 11 revised full papers were carefully reviewed and selected from 29 submissions. In addition to the 11 papers, this volume includes 3 abstracts of invited talks and 2 abstracts of invited tutorials. the papers are grouped into the following topics: analysis of term rewriting; logic-based distributed/concurrent programming; analysis of logicprogramming; and program analysis.
Computational systems based on a first-order language that can be given a canonical model which captures provability in the corresponding calculus can often be seen as first-order theories S, and computational propert...
详细信息
ISBN:
(纸本)9783319944609;9783319944593
Computational systems based on a first-order language that can be given a canonical model which captures provability in the corresponding calculus can often be seen as first-order theories S, and computational properties of such systems can be formulated as first-order sentences. that hold in such a canonical model of S. In this setting, standard results regarding the preservation of satisfiability of different classes of first-order sentences yield a number of interesting applications in program analysis. In particular, properties expressed as existentially quantified boolean combinations of atoms (for instance, a set of unification problems) can then be disproved by just finding an arbitrary model of the considered theory plus the negation of such a sentence. We show that rewriting-based systems fit into this approach. Many computational properties (e.g., infeasibility and non-joinability of critical pairs in (conditional) rewriting, non-loopingness, or the secure access to protected pages of a web site) can be investigated in this way. Interestingly, this semantic approach succeeds when specific techniques developed to deal withthe aforementioned problems fail.
Fuzzy logicprogramming is a growing declarative paradigm aiming to integrate fuzzy logic into logicprogramming. One of the most difficult tasks when specifying a fuzzy logicprogram is determining the right weights ...
详细信息
ISBN:
(纸本)9783319631394;9783319631387
Fuzzy logicprogramming is a growing declarative paradigm aiming to integrate fuzzy logic into logicprogramming. One of the most difficult tasks when specifying a fuzzy logicprogram is determining the right weights for each rule, as well as the most appropriate fuzzy connectives and operators. In this paper, we introduce a symbolic extension of fuzzy logicprograms in which some of these parameters can be left unknown, so that the user can easily see the impact of their possible values. Furthermore, given a number of test cases, the most appropriate values for these parameters can be automatically computed. Finally, we show some benchmarks that illustrate the usefulness of our approach.
State-of-the-art answer set programming (ASP) solvers rely on a program called a grounder to convert non-ground programs containing variables into variable-free, propositional programs. the size of this grounding depe...
详细信息
ISBN:
(纸本)9783319631394;9783319631387
State-of-the-art answer set programming (ASP) solvers rely on a program called a grounder to convert non-ground programs containing variables into variable-free, propositional programs. the size of this grounding depends heavily on the size of the non-ground rules, and thus, reducing the size of such rules is a promising approach to improve solving performance. To this end, in this paper we announce lpopt, a tool that decomposes large logicprogramming rules into smaller rules that are easier to handle for current solvers. the tool is specifically tailored to handle the standard syntax of the ASP language (ASP-Core) and makes it easier for users to write efficient and intuitive ASP programs, which would otherwise often require significant hand-tuning by expert ASP engineers. It is based on an idea proposed by Morak and Woltran (2012) that we extend significantly in order to handle the full ASP syntax, including complex constructs like aggregates, weak constraints, and arithmetic expressions. We present the algorithm, the theoretical foundations on how to treat these constructs, as well as an experimental evaluation showing the viability of our approach.
暂无评论