An experiment is described that confirms the security of a well-studied class of cryptographic protocols (Dolev-Yao intruder model) can be verified by two-way nondeterministic pushdown automata (2NPDA). A nondetermini...
详细信息
An experiment is described that confirms the security of a well-studied class of cryptographic protocols (Dolev-Yao intruder model) can be verified by two-way nondeterministic pushdown automata (2NPDA). A nondeterministic pushdown program checks whether the intersection of a regular language (the protocol to verify) and a given Dyck language containing all canceling words is empty. If it is not, an intruder can reveal secret messages sent between trusted users. The verification is guaranteed to terminate in cubic time at most on a 2NPDA-simulator. The interpretive approach used in this experiment simplifies the verification, by separating the nondeterministic pushdown logic and program control, and makes it more predictable. We describe the interpretive approach and the known transformational solutions, and show they share interesting features. Also noteworthy is how abstract results from automata theory can solve practical problems by programming language means.
This paper attempts a direct semantic formalization of first-order relational-functional languages (the characteristic RELFUN subset) in terms of a generalized model concept. Function-defining conditional equations (o...
详细信息
The proceedings contain 18 papers. The special focus in this conference is on Functional and logicprogramming. The topics include: Safe folding/unfolding with conditional narrowing;optimal non-deterministic functiona...
ISBN:
(纸本)3540634592
The proceedings contain 18 papers. The special focus in this conference is on Functional and logicprogramming. The topics include: Safe folding/unfolding with conditional narrowing;optimal non-deterministic functional logic computations;a semantic basis for termination analysis of logic programs and its realization using symbolic norm constraints;parallelizing functional programs by generalization;higher-order equational unification via explicit substitutions;parameterised higher-order algebraic specifications;a computation model for a higher-order functional logic language;on composable properties of term rewriting systems;needed reductions with context-sensitive rewriting;conditional term graph rewriting;lazy narrowing with parametric order sorted types;termination of algebraic type systems;proof net semantics of proof search computation;perpetuality and uniform normalization;model generation with existentially quantified variables and constraints and optimal left-to-right pattern-matching automata.
We present the first tableau method with an EXPTIME (optimal) complexity for checking satisfiability of a knowledge base in the description logic SHOQ, which extends ALC with transitive roles, hierarchies of roles, no...
详细信息
We present the first tableau method with an EXPTIME (optimal) complexity for checking satisfiability of a knowledge base in the description logic SHOQ, which extends ALC with transitive roles, hierarchies of roles, nominals and quantified number restrictions. The complexity is measured using binary representation for numbers. Our procedure is based on global caching and integer linear feasibility checking.
In this paper we describe a novel approach to programming microcontrollers based on the Arduino platform using Datalog as a clear and concise description language for system behaviors. The application areas of cheap a...
详细信息
We present a method for specifying and implementing algorithms for Boolean logic problems. It is formally grounded in relational algebra. Specifications are written in first-order set theory and then transformed syste...
详细信息
The proceedings contain 7 papers. The topics discussed include: mining fix patterns with context information for automatic program repair;quick repair of semantic errors for debugging;FixEval: execution-based evaluati...
ISBN:
(纸本)9798350302141
The proceedings contain 7 papers. The topics discussed include: mining fix patterns with context information for automatic program repair;quick repair of semantic errors for debugging;FixEval: execution-based evaluation of program fixes for programming problems;program repair competition;beyond code generation: the need for type-aware language models;an analysis of the automatic bug fixing performance of ChatGPT;and an extensive study on model architecture and program representation in the domain of learning-based automated program repair.
In order to properly test software, test data of a certain quality is needed. However, useful test data is often unavailable because existing or hand-crafted data might not be diverse enough to enable desired test cas...
详细信息
The proceedings contain 23 papers. The special focus in this conference is on Compiler Compilers. The topics include: Using an LALR compiler compiler to generate incremental parsers;generating efficient code from cont...
ISBN:
(纸本)9783540536697
The proceedings contain 23 papers. The special focus in this conference is on Compiler Compilers. The topics include: Using an LALR compiler compiler to generate incremental parsers;generating efficient code from continuation semantics;Optimizing directly executable LR parsers;SYS/3 – a software development tool;An attributed ELL(1)-parser generator;a hybrid top-down parsing technique;computer-aided building of a compiler: An example;specification and implementation of a tree-abiding interface for ada;towards a multilingual natural language understanding interface;Application development with the FNC-2 attribute grammar system;mixed dialogue control defined by an attribute grammar;mate – a metasystem with concurrent attribute evaluation;A practical implementation of DCGs;algorithmic debugging for imperative languages with side-effects;compilation for instruction parallel processors;a generator for production quality compilers;rie and Jun: Towards the generation of all compiler phases;STARLET : An affix-based compiler compiler designed as a logicprogramming system;PAGODE: A back end generator using attribute abstract syntaxes and term rewritings;a tool box for compiler construction;tools and techniques of annotated programming.
Creation of customized animated 3D content is an important issue in web-based VR/AR environments that involve users with various requirements for the content, e.g., in education, training, tourism, cultural heritage a...
详细信息
Creation of customized animated 3D content is an important issue in web-based VR/AR environments that involve users with various requirements for the content, e.g., in education, training, tourism, cultural heritage and e-commerce. 3D content customization is a complex task, as it typically covers various content features such as geometry, structure and appearance. Although a number of tools enable modeling of 3D animations, they do not support on-demand animation customization to users' requirements specified using semantic (application or domain-specific) concepts. Available solutions permit creation of 3D content in its final form, require technical knowledge and skills or are limited to a particular application domain, without possibilities to easily change the target application or domain. In this paper, we present a pipeline for creation of customized animated 3D content on the web. The pipeline uses rule-based representation of 3D content activities, which are composed into more complex animations. Animation composition is performed on-demand, using queries describing requirements in an arbitrary application domain. The use of knowledgerepresentation adapts the approach to the current trends in the evolution of the web, including the semantic web. It enables exploration by reasoning on the content generated with users' queries. Furthermore, it permits inference of tacit properties of animations from explicitly specified properties, thereby liberating the authors from specifying all necessary animation properties. The pipeline leverages an advanced motion capture system, 3D modeling tools and game engines. We have implemented and evaluated a web-based environment for on-demand animation composition. The proposed approach can be successfully used in multiple application areas on the web, in which 3D content components are intensively reconfigured according to requirements of different users.
暂无评论