this paper describes a compositional analysis algorithm for statically detecting leaks in Java programs. the algorithm is based on separation logic and exploits the concept of bi-abductive inference for identifying th...
详细信息
ISBN:
(纸本)9783642120282
this paper describes a compositional analysis algorithm for statically detecting leaks in Java programs. the algorithm is based on separation logic and exploits the concept of bi-abductive inference for identifying the objects which are reachable but no longer used by the program.
the theory BV of bit-vectors, i.e. fixed-size arrays of bits equipped with standard low-level machine instructions, is becoming very popular in formal verification. Standard solvers for this theory are based on a bit-...
详细信息
ISBN:
(纸本)9783642120015
the theory BV of bit-vectors, i.e. fixed-size arrays of bits equipped with standard low-level machine instructions, is becoming very popular in formal verification. Standard solvers for this theory are based on a bit-level encoding into propositional logic and SAT-based resolution techniques. In this paper, we investigate an alternative approach based on a word-level encoding into bounded arithmetic and Constraint logicprogramming (CLP) resolution techniques. We define an original CLP framework (domains and propagators) dedicated to bit-vector constraints. this framework is implemented in a prototype and thorough experimental studies have been conducted. the new approach is shown to perform much better than standard CLP-based approaches, and to considerably reduce the gap withthe best SAT-based BV solvers.
thanks to the high expressive power and the rule-based nature of declarative languages, their influences are growing in the fields of AI, knowledge representation, and so on. On the other hand, since the notion of &qu...
详细信息
ISBN:
(纸本)9783642140549
thanks to the high expressive power and the rule-based nature of declarative languages, their influences are growing in the fields of AI, knowledge representation, and so on. On the other hand, since the notion of "equality" plays a crucial role on such languages, in this paper we focus in the design of a flexible (fuzzy) but efficient (lazy) notion of equality for hybrid declarative languages amalgamating functional-fuzzy-logic features. Here, we show that, by extending at a very low cost the notion of "strict equality" typically used in lazy functional-logic languages (Curry, Toy), and by relaxing it to the more flexible one of similar equality used in fuzzy-logicprogramming languages (Likelog, Bousi similar to Prolog), similarity relations can be successfully treated while mathematical functions are lazily evaluated in a given program. Our method represents a very easy, low-cost way, for fuzzifying lazy functional-logic languages and it can be implemented at a very high abstraction level by simply performing a static pre-process at compilation time which only manipulates the program at a syntactic level (i.e., the underlying operational mechanism based on rewriting/narrowing remains untouched).
Over the past couple of decades, a series of exact exponential-time algorithms have been developed with improved run times for a number of problems including IndependentSet, k-SAT, and k-colorability using a variety o...
详细信息
ISBN:
(数字)9783642141867
ISBN:
(纸本)9783642141850
Over the past couple of decades, a series of exact exponential-time algorithms have been developed with improved run times for a number of problems including IndependentSet, k-SAT, and k-colorability using a variety of algorithmic techniques such as backtracking, dynamic programming, and inclusion-exclusion. the series of improvements are typically in the form of better exponents compared to exhaustive search. these improvements prompt several questions, chief among them is whether we can expect continued improvements in the exponent. Is there a limit beyond which one should not expect improvement? If we assume NP ≠ P or other appropriate complexity statement, what can we say about the likely exact complexities of various NP-complete problems?
the proceedings contain 56 papers. the topics discussed include: a unified approach to modeling and programming;generic meta-modeling with concepts, templates and mixing layers;an observer-based notion of model inheri...
ISBN:
(纸本)3642161286
the proceedings contain 56 papers. the topics discussed include: a unified approach to modeling and programming;generic meta-modeling with concepts, templates and mixing layers;an observer-based notion of model inheritance;a comparison of model migration tools;active operations on collections;a technique for automatic validation of model transformations;verifying semantic conformance of state machine-to-java code generators;a dynamic-priority based approach to fixing inconsistent feature models;taming graphical modeling;application logic patterns - reusable elements of user-system interaction;a metamodel-based approach for automatic user interface generation;improving test models for large scale industrial systems: an inquisitive study;scaling up model driven engineering - experience and lessons learnt;modeling issues: a survival guide for a non-expert modeler;and model-to-metamodel transformation for the development of component-based systems.
the proceedings contain 56 papers. the topics discussed include: a unified approach to modeling and programming;generic meta-modeling with concepts, templates and mixing layers;an observer-based notion of model inheri...
ISBN:
(纸本)3642161448
the proceedings contain 56 papers. the topics discussed include: a unified approach to modeling and programming;generic meta-modeling with concepts, templates and mixing layers;an observer-based notion of model inheritance;a comparison of model migration tools;active operations on collections;a technique for automatic validation of model transformations;verifying semantic conformance of state machine-to-java code generators;a dynamic-priority based approach to fixing inconsistent feature models;taming graphical modeling;application logic patterns - reusable elements of user-system interaction;a metamodel-based approach for automatic user interface generation;improving test models for large scale industrial systems: an inquisitive study;scaling up model driven engineering - experience and lessons learnt;modeling issues: a survival guide for a non-expert modeler;and model-to-metamodel transformation for the development of component-based systems.
Recently, several unsatisfiability-based algorithms have been proposed for Maximum Satisfiability (MaxSAT) and other Boolean Optimization problems. these algorithms are based on being able to iteratively identify and ...
详细信息
ISBN:
(数字)9783642141867
ISBN:
(纸本)9783642141850
Recently, several unsatisfiability-based algorithms have been proposed for Maximum Satisfiability (MaxSAT) and other Boolean Optimization problems. these algorithms are based on being able to iteratively identify and relax unsatisfiable sub-formulas withthe use of fast Boolean satisfiability solvers. It has been shown that this approach is very effective for several classes of instances, but it can perform poorly on others for which classical Boolean optimization algorithms find it easy to solve. this paper proposes the use of Pseudo-Boolean Optimization (PBO) solvers as a preprocessor for unsatisfiability-based algorithms in order to increase its robustness. Moreover, the use of constraint branching, a well-known technique from integer Linear programming, is also proposed into the unsatisfiability-based framework. Experimental results show that the integration of these features in an unsatisfiability-based algorithm results in an improved and more effective solver for Boolean optimization problems.
this paper focuses on a logical model of induction, and specifically of the common machine learning task of inductive concept learning (ICL). We define an inductive derivation relation, which characterizes which hypot...
详细信息
ISBN:
(纸本)9781607506430;9781607506423
this paper focuses on a logical model of induction, and specifically of the common machine learning task of inductive concept learning (ICL). We define an inductive derivation relation, which characterizes which hypothesis can be induced from sets of examples, and show its properties. Moreover, we will also consider the problem of communicating inductive inferences between two agents, which corresponds to the multi-agent ICL problem. thanks to the introduced logical model of induction, we will show that this communication can be modeled using computational argumentation.
All large transport aircraft are required to be equipped with a collision avoidance system that instructs pilots how to maneuver to avoid collision with other aircraft. the uncertainty in the behavior of the intruding...
详细信息
All large transport aircraft are required to be equipped with a collision avoidance system that instructs pilots how to maneuver to avoid collision with other aircraft. the uncertainty in the behavior of the intruding aircraft makes developing a robust collision avoidance logic challenging. this paper presents an automated approach for optimizing collision avoidance logic based on probabilistic models of aircraft behavior and a performance metric that balances the competing objectives of maximizing safety and minimizing alert rate. the approach involves framing the problem of collision avoidance as a Markov decision process that is solved using dynamic programming. Although this paper focuses on airborne collision avoidance for manned aircraft, the methods may be applied to collision avoidance for other categories of vehicles, both manned and unmanned.
the logic FO(ID) uses ideas from the field of logicprogramming to extend first order logic with non-monotone inductive definitions. the goal of this paper is to extend Gentzen's sequeut calculus to obtain a deduc...
详细信息
ISBN:
(纸本)9783642042379
the logic FO(ID) uses ideas from the field of logicprogramming to extend first order logic with non-monotone inductive definitions. the goal of this paper is to extend Gentzen's sequeut calculus to obtain a deductive inference method for FO(ID). the main difficulty in building Such a proof system is the representation and inference of unfounded sets. It turns out that we can represent unfounded sets by least fixpoint expressions borrowed from stratified least fixpoint logic (SLFP), which is a logic with a least fixpoint operator and characterizes the expressibility of stratified logic programs. therefore, in this paper, we integrate least fixpoint expressions into FO(ID) and define the logic FO(ID,SLFP). We investigate a sequeut calculus for FO(ID,SLFP), which extends the sequent calculus for SLFP with inference rules for the inductive definitions of FO(ID). We show that this proof system is sound with respect to a slightly restricted fragment of FO(ID) and complete for a more restricted fragment of FO(ID).
暂无评论