this paper explores an approach to design for verification in systems built atop a middleware framework which separates synchronization concerns from the "core-functional logic" of a program. the framework i...
详细信息
this paper explores an approach to design for verification in systems built atop a middleware framework which separates synchronization concerns from the "core-functional logic" of a program. the framework is based on a language-independent compositional model of synchronization contracts, called Szumo, which integrates well with popular OO design artifacts and provides strong guarantees of non-interference for a class of strictly exclusive systems. An approach for extracting models from Szumo design artifacts and analyzing the generated models to detect deadlocks is described. A key decision was to use Constraint Handling Rules to express the semantics of synchronization contracts, which allowed a transparent model of the implementation logic.
this paper develops a new semantic framework that supports employee performance appraisals, based on inductive logicprogramming and data mining techniques. the framework is applied to learn a grammar for writing SMAR...
详细信息
the proceedings contain 13 papers. the special focus in this conference is on Formal Aspects of Component Software. the topics include: Realisability of Branching Pomsets;liquidity Analysis in Resource-Aware...
ISBN:
(纸本)9783031208713
the proceedings contain 13 papers. the special focus in this conference is on Formal Aspects of Component Software. the topics include: Realisability of Branching Pomsets;liquidity Analysis in Resource-Aware programming;open Compliance in Multiparty Sessions;specifying Source Code and Signal-based Behaviour of Cyber-Physical System Components;formally Characterizing the Effect of Model Transformations on System Properties;interpretation and Formalization of the Right-of-Way Rules;formal Model In-the-Loop for Secure Industrial Control Networks;Debugging of BPMN Processes Using Coloring Techniques;WEASY: A Tool for Modelling Optimised BPMN Processes;embeddings Between State and Action Based Probabilistic logics;footprint logic for Object-Oriented Components.
this paper concerns formal theories for reasoning about the knowledge and belief of agents. It has seemed attractive to researchers in artificial intelligence to formalise these propositional attitudes as predicates o...
详细信息
this paper concerns formal theories for reasoning about the knowledge and belief of agents. It has seemed attractive to researchers in artificial intelligence to formalise these propositional attitudes as predicates of first-order predicate logic. this allows the agents to express stronger introspective beliefs and engage in stronger meta-rcasoning than in the classical modal operator approach. Results by Montague [1963] and thomason [1980] show, however, that the predicate approach is prone to inconsistency. More recent results by des Rivieres & Levesque [1988] and Morreau & Kraus [1998] show that we can maintain the predicate approach if we make suitable restrictions to our set of epistemic axioms. their results are proved by careful translations from corresponding modal formalisms. In the present paper we show that their results fit nicely into the framework of logicprogramming semantics, in that we show their results to be corollaries of well-known results in this field. this does not only allow us to demonstrate a close connection between consistency problems in the syntactic treatment of propositional attitudes and problems in semantics for logic programs, but it also allows us to strengthen the results of des Rivieres & Levesque [1988] and Morreau & Kraus [1998].
this book constitutes the thoroughly refereed post-conference proceedings of the 18thinternational Symposium on logic-Based Program Synthesis and Transformation, LOPSTR 2008, held in Valencia, Spain, during July 17-1...
详细信息
ISBN:
(数字)9783642005152
ISBN:
(纸本)9783642005145
this book constitutes the thoroughly refereed post-conference proceedings of the 18thinternational Symposium on logic-Based Program Synthesis and Transformation, LOPSTR 2008, held in Valencia, Spain, during July 17-18, 2008. the 11 revised full papers presented together with one invited talk were carefully reviewed and selected for inclusion in the book. LOPSTR traditionally solicits papers in the areas of specification, synthesis, verification, transformation, analysis, optimization, composition, security, reuse, applications and tools, component-based software development, software architectures, agent-based software development, and program refinement.
Intelligent robotic assistants can potentially improve the quality of life for elderly people and help them maintain their independence. However, the number of different and personalized tasks render pre-programming o...
详细信息
ISBN:
(纸本)9781538672839
Intelligent robotic assistants can potentially improve the quality of life for elderly people and help them maintain their independence. However, the number of different and personalized tasks render pre-programming of such assistive robots prohibitively difficult. Instead, to cope with a continuous and open-ended stream of cooperative tasks, new collaborative skills need to be continuously learned and updated from demonstrations. To this end, we introduce an online learning method for a skill library of collaborative tasks that employs an incremental mixture model of probabilistic interaction primitives. this model chooses a corresponding robot response to a human movement where the human intention is extracted from previously demonstrated movements. Unlike existing batch methods of movement primitives for humanrobot interaction, our approach builds a library of skills online, in an open-ended fashion and updates existing skills using new demonstrations. the resulting approach was evaluated both on a simple benchmark task and in an assistive human-robot collaboration scenario with a 7DoF robot arm.
the proceedings contain 41 papers. the topics discussed include: C-SHORe: a collapsible approach to higher-order verification;exploiting vector instructions with generalized stream fusion;type-theory in color;Mtac: a ...
ISBN:
(纸本)9781450323260
the proceedings contain 41 papers. the topics discussed include: C-SHORe: a collapsible approach to higher-order verification;exploiting vector instructions with generalized stream fusion;type-theory in color;Mtac: a monad for typed tactic programming in Coq;fun with semirings: a functional pearl on the abuse of linear algebra;programming and reasoning with algebraic effects and dependent types;well-founded recursion with copatterns: a unified approach to termination and productivity;productive coprogramming with guarded recursion;higher-order functional reactive programming without spacetime leaks;simple and compositional reification of monadic embedded languages;structural recursion for querying ordered graphs;a nanopass framework for commercial compiler development;the bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier;and a practical theory of language-integrated query.
the proceedings contain 76 papers. the topics discussed include: selfish distributed optimization;tulipse: a visualization framework for user-guided parallelization;pattern-independent detection of manual collectives ...
ISBN:
(纸本)9783642328190
the proceedings contain 76 papers. the topics discussed include: selfish distributed optimization;tulipse: a visualization framework for user-guided parallelization;pattern-independent detection of manual collectives in MPI programs;a type-based approach to separating protocol from application logic: a case study in hybrid computer programming;energy consumption modeling for hybrid computing;HPC file systems in wide area networks: understanding the performance of luster over wan;understanding I/O performance using I/O skeletal applications;CRAW/P: a workload partition method for the efficient parallel simulation of manycores;job scheduling using successive linear programming approximations of a sparse model;speed scaling on parallel processors with migration;dynamic distributed scheduling algorithm for state space search;and using load information in work-stealing on distributed systems with non-uniform communication latencies.
the problem of determining the Worse Case Execution Time (WCET) of a piece of code is a fundamental one in the Real Time Systems community. Existing methods either try to gain this information by analysis of the progr...
详细信息
ISBN:
(纸本)9783540859277
the problem of determining the Worse Case Execution Time (WCET) of a piece of code is a fundamental one in the Real Time Systems community. Existing methods either try to gain this information by analysis of the program code or by running extensive timing analyses. this paper presents a new approach to the problem based on using Machine Learning in the form of ILP to infer program properties based on sample executions of the code. Additionally, significant improvements in the range of functions learnable and the time taken for learning can be made by the application of more advanced ILP techniques.
We investigate the combination of answer set programming and qualitative optimization techniques. Answer set optimization programs (ASO programs) have two parts. the generating program Pyen produces answer sets repres...
详细信息
We investigate the combination of answer set programming and qualitative optimization techniques. Answer set optimization programs (ASO programs) have two parts. the generating program Pyen produces answer sets representing possible solutions. the preference program Ppref expresses user preferences. It induces a preference relation on the answer sets of Pyen based on the degree to which rules are satisfied. We discuss possible applications of ASO programming, give complexity results and propose implementation techniques. We also analyze the relationship between A SO programs and CP-networks.
暂无评论