Static analysis of binary code is challenging for several reasons. In particular, standard static analysis techniques operate over control-flow graphs, which are not available when dealing with self-modifying programs...
详细信息
Static analysis of binary code is challenging for several reasons. In particular, standard static analysis techniques operate over control-flow graphs, which are not available when dealing with self-modifying programs which can modify their own code at runtime. We formalize in the Coq proof assistant some key abstract interpretation techniques that automatically extract memory safety properties from binary code. Our analyzer is formally proved correct and has been run on several self-modifying challenges, provided by Cai et al. in their PLDI 2007 article.
Multi-adjoint logic programs were recently proposed as a generalization of monotonic and residuated logic programs, in that simultaneous use of several implications in the rules and rather general connectives in the b...
详细信息
ISBN:
(纸本)3540222189
Multi-adjoint logic programs were recently proposed as a generalization of monotonic and residuated logic programs, in that simultaneous use of several implications in the rules and rather general connectives in the bodies are allowed. In this work, the need of biresiduated pairs is justified through the study of a very intuitive family of operators, which turn out to be not necessarily commutative and associative and, thus, might have two different residuated implications;finally, we introduce the framework of biresiduated multi-adjoint logicprogramming and sketch some considerations on its fixpoint semantics.
A parser formalism for natural languages that is so restricted as to rule out the definition of linguistic structures that do not occur in any natural language can make the task of grammar construction easier, whether...
详细信息
the proceedings contain 11 papers. the topics discussed include: translating NP-SPEC into ASP;SPARC – sorted asp with consistency restoring rules;utilizing asp for generating and visualizing argumentation frameworks;...
the proceedings contain 11 papers. the topics discussed include: translating NP-SPEC into ASP;SPARC – sorted asp with consistency restoring rules;utilizing asp for generating and visualizing argumentation frameworks;planning and scheduling in hybrid domains using answer set programming;eliminating unfounded set checking for HEX-programs;backdoors to normality for disjunctive logic programs;answer set programming for stream reasoning;and two new definitions of stable models of logic programs with generalized quantifiers.
logicprogramming is a prominent approach for knowledge representation and reasoning. Answer set semantics of logic. programs provides a promising constraint programming paradigm. Consistency is a significant issue in...
详细信息
ISBN:
(纸本)9780769533056
logicprogramming is a prominent approach for knowledge representation and reasoning. Answer set semantics of logic. programs provides a promising constraint programming paradigm. Consistency is a significant issue in answer set programming. We investigated the order consistent logic programs and showed that the class of order consistent logic programs is identical to the call consistent one for finite logic programs, order consistency is decidable in polynomial time and Lifschitz's order consistency is identical to Sato's definition.
In recent years logicprogramming based languages and features such as rules and non-monotonic constructs have become important in various knowledge representation paradigms. While the early logicprogramming language...
详细信息
ISBN:
(纸本)9783642239625;9783642239632
In recent years logicprogramming based languages and features such as rules and non-monotonic constructs have become important in various knowledge representation paradigms. While the early logicprogramming languages, such as Horn logic programs and Prolog did not focus on expressing and reasoning with uncertainty, in recent years logicprogramming languages have been developed that can express bothlogical and quantitative uncertainty. In this paper we give an overview of such languages and the kind of uncertainty they can express and reason with. Among those, we slightly elaborate on the language P-log that not only accommodates probabilistic reasoning, but also respects causality and distinguishes observational and action updates.
this paper introduces Chronolog(Z), a logicprogramming language based on a discrete linear-time temporal logic with unbounded past and future. Chronolog(Z) is suitable for applications involving the notion of dynamic...
详细信息
We certify in the proof assistant Isabelle/HOL the soundness of a declarative first-order prover with equality. the LCF-style prover is a translation we have made, to Standard ML, of a prover in John Harrison's Ha...
详细信息
We certify in the proof assistant Isabelle/HOL the soundness of a declarative first-order prover with equality. the LCF-style prover is a translation we have made, to Standard ML, of a prover in John Harrison's Handbook of Practical logic and Automated Reasoning. We certify it by replacing its kernel with a certified version that we program, certify and generate code from;all in Isabelle/HOL. In a declarative proof each step of the proof is declared, similar to the sentences in a thorough paper proof. the prover allows proofs to mix the declarative style with automatic theorem proving by using a tableau prover. Our motivation is teaching how automated and declarative provers work and how they are used. the prover allows studying concrete code and a formal verification of correctness. We show examples of proofs and how they are made in the prover. the entire development runs in Isabelle's ML environment as an interactive application or can be used standalone in OCaml or Standard ML (or in other functional programming languages like Haskell and Scala with some additional work).
In this paper we continue the work on our extension of Answer Set programming by non-Herbrand functions and add to the language support for arithmetic expressions and various inequality relations over non-Herbrand fun...
详细信息
A system has been designed and implemented to remotely configure generic automated systems using only conditional logic statements and a web-based application for intuitive user interaction. Current automation systems...
详细信息
ISBN:
(纸本)9789811031533;9789811031526
A system has been designed and implemented to remotely configure generic automated systems using only conditional logic statements and a web-based application for intuitive user interaction. Current automation systems use company-specific applications and require manual configuring in order to make any changes as per the user's needs. the purpose of this system is to give users the ability to self-configure and control all their systems from anywhere, using a simple internet-based application, thus requiring no external intervention. Our system is built using open-source software and hardware, thus rendering it cost-effective to implement in real time. Conditional programming, or If-then-Else logic, has been used as it is an easily understandable logic construct to maintain and configure the automated systems.
暂无评论