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.
We propose an automated technique for inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based structures and heap manipulation. Starting ...
详细信息
ISBN:
(纸本)9783319631394;9783319631387
We propose an automated technique for inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KernelC in the K framework, we enrich the symbolic execution facilities recently provided by C with novel capabilities for assertion synthesisthat are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that explains the execution of a (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KindSpec 2.0, which generates logical axioms that define the precise input/ output behavior of the C routines.
this paper presents an analysis to infer range and value-set information for programs operating on programmable logic controllers. Given a program, the algorithm gathers all possible values of all variables for all po...
详细信息
ISBN:
(纸本)9783902823281
this paper presents an analysis to infer range and value-set information for programs operating on programmable logic controllers. Given a program, the algorithm gathers all possible values of all variables for all possible program executions using abstract simulation. the set of these values constitutes an over-approximation of the program behavior and can thus be used to directly detect potential misbehavior. Crucially for practical applications, this approach works automatically without preprocessing or manual intervention. the approach is implemented in the Arcade. PLC framework and evaluated on a case study from industry.
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.
Type information has many applications;it can e.g. be used in optimized compilation, termination analysis and error detection. However, logicprograms are typically untyped. A well-typed program has the property that ...
详细信息
ISBN:
(纸本)9783642005145
Type information has many applications;it can e.g. be used in optimized compilation, termination analysis and error detection. However, logicprograms are typically untyped. A well-typed program has the property that it behaves identically on well-typed goals with or without type checking. Hence the automatic inference of a well-typing is worthwhile. Existing inferences are either cheap and inaccurate, or accurate and expensive. By giving up the requirement that all calls to a predicate have types that are instances of a unique polymorphic type but instead allowing multiple polymorphic typings for the same predicate, we obtain a novel strongly-connected-component-based analysis that provides a good compromise between accuracy and computational cost.
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.
this paper describes rules to transform Verilog HDL source code in order to propagate X-values on RTL models in a more realistic way, and to check for potential differences of RTL simulation results against expected s...
详细信息
this paper describes rules to transform Verilog HDL source code in order to propagate X-values on RTL models in a more realistic way, and to check for potential differences of RTL simulation results against expected silicon implementation behavior. By running X-propagation simulations in parallel to usual RTL simulation and debugging, RTL design bugs previously detected in gate-level simulations can be detected earlier now. A prototypical tool automatically implements the proposed transformation rules. Experimental results on two industrial hardware designs validate the usefulness of our approach and justify its application in everyday use.
Service-based Systems (SBS) are being adopted by many distributed systems. Applications in SBS can often be viewed as the composition of various computing services following specific workflows. these workflows often n...
详细信息
ISBN:
(纸本)9780769528106
Service-based Systems (SBS) are being adopted by many distributed systems. Applications in SBS can often be viewed as the composition of various computing services following specific workflows. these workflows often need to satisfy various timing and resource constraints. In this paper, a software cybernetics approach to deploying and scheduling workflows with timing and resource constraints in SBS is presented In our approach, a logic-based technique for modeling and solving timing and resource constraints for workflows in SBS is developed to generate the initial resource assignments, schedules and deployment plans of agents for workflows. the principles and concepts in software cybernetics are applied to guide the synthesis of software controllers for monitoring and adapting system behavior.
Algorithmic debugging is a debugging technique that has been extended to practically all programming paradigms. It is based on the answers of the programmer to a series of questions generated automatically by the algo...
详细信息
ISBN:
(纸本)9783540714095
Algorithmic debugging is a debugging technique that has been extended to practically all programming paradigms. It is based on the answers of the programmer to a series of questions generated automatically by the algorithmic debugger. therefore, the performance of the technique is strongly dependent on the number and the complexity of these questions. In this work we overview and compare current strategies for algorithmic debugging and we introduce some new strategies and discuss their advantages over previous approaches.
暂无评论