The proceedings contain 27 papers. The special focus in this conference is on Real-Time Systems, Formally Engineering Systems, Software Engineering and Object Orientation. The topics include: An essay on software engi...
ISBN:
(纸本)3540672613
The proceedings contain 27 papers. The special focus in this conference is on Real-Time Systems, Formally Engineering Systems, Software Engineering and Object Orientation. The topics include: An essay on software engineering at the turn of century;parallel refinement mechanisms for real-time systems;a process algebra for real-time programs;system fault tolerance specification;proposal of a method combining semi-formal and formal approaches;structuring and design of reactive systems using RSDS and b;using domain-specific languages for the realization of component composition;analysing UML active classes and associated state machines;quality factors and life-cycle revised;a formal approach to heterogeneous software modeling;formal specification of object-oriented meta-modelling;verification of object oriented programs using class invariants;verification of object-z specifications by using transition systems;application to the radiomobile network design problem;a model for describing object-oriented systems from multiple perspectives;stepwise introduction and preservation of safety properties in algebraic high-level net systems;ready-simulation is not ready to express a modular refinement relation;java program verification via a Hoare logic with abrupt termination;foundations for software configuration management policies using graph transformations;analyzing non-functional properties of mobile agents;specification of an automatic manufacturing system;a case study on using automata in control synthesis and formal system development with KIV.
The proceedings contain 36 papers. The special focus in this conference is on Software, Formal Methods Tools, Hybrid Systems, Parameterized Systems and Efficient Model-Checking. The topics include: On the construction...
ISBN:
(纸本)3540672826
The proceedings contain 36 papers. The special focus in this conference is on Software, Formal Methods Tools, Hybrid Systems, Parameterized Systems and Efficient Model-Checking. The topics include: On the construction of automata from linear arithmetic constraints;an extensible type system for component-based design;viewpoint-oriented software development;tool support for integrating multiple perspectives by distributed graph transformation;an architecture for interactive program provers;on memory-block traversal problems in model-checking timed systems;symbolic model checking for rectangular hybrid systems;efficient data structure for fully symbolic verification of real-time software systems;verification of parameterized systems using logic program transformations;abstracting ws1s systems to verify parameterized networks;a tool for expressing validation techniques over infinite state systems;transitive closures of regular relations for verifying infinite-state systems;using static analysis to improve automatic test generation;efficient diagnostic generation for Boolean equation systems;compositional state space generation with partial order reductions for asynchronous communicating systems;checking for CFFD-preorder with tester processes;integrating low level symmetries into reachability analysis;model checking support for the ASM high-level language;combining constraint solvers with BDDS for automatic invariant checking;symbolic reachability analysis based on sat-solvers;symbolic representation of upward-closed sets;an experimental evaluation for asynchronous concurrent systems and tool-based specification of visual languages and graphic editors.
作者：
Bistarelli, S.Gennari, R.Rossi, F.Università di Pisa
Dipartimento di Informatica Corso Italia 40 Pisa56125 Italy ILLC
Institute of Logic Language and Computation University of Amsterdam N. Doelenstraat 15 Amsterdam1012 CP Netherlands Università di Padova
Dipartimento di Matematica Pura ed Applicata Via Belzoni 7 Padova35131 Italy
Soft constraints based on semirings are a generalization of classical constraints, where tuples of variables’ values in each soft constraint are uniquely associated to elements from an algebraic structure called semi...
详细信息
Learning from examples is an important branch of inductive learning, and is also the bottle-neck in concepts extraction of machine learning. Based on inductive learning theory, this paper applies combinatorial optimiz...
详细信息
ISBN:
(纸本)7312012035
Learning from examples is an important branch of inductive learning, and is also the bottle-neck in concepts extraction of machine learning. Based on inductive learning theory, this paper applies combinatorial optimization method to setup the programming models of learning concepts of the prepositional logic formulas in the conjunctive normal form (CNF) and disjunctive normal form (DNF). Then, genetic algorithms (GA), specified to CNF learning, is designed. GA can find the multiple optimal solution in theory and practice, and experiments reveal that it runs more efficiently compared with heuristic algorithms of the GS type.
Declarative programming languages, are high-level programming languages in which one only has to state what is to be computed and not necessarily how it is to be computed. logicprogramming and functional programming ...
ISBN:
(纸本)3540667105
Declarative programming languages, are high-level programming languages in which one only has to state what is to be computed and not necessarily how it is to be computed. logicprogramming and functional programming are two prominent members of this class of programming languages. While functional programming is based on the λ-calculus, logicprogramming has its roots in first-order logic and automated theorem proving. Both approaches share the view that a program is a theory and execution consists in performing deduction from that theory.
A Hoare-style programminglogic for the sequential kernel of Java is presented. It handles recursive methods, class and interface types, subtyping, inheritance, dynamic and static binding, aliasing via object referenc...
详细信息
ISBN:
(纸本)3540656995
A Hoare-style programminglogic for the sequential kernel of Java is presented. It handles recursive methods, class and interface types, subtyping, inheritance, dynamic and static binding, aliasing via object references, and encapsulation. The logic is proved sound w.r.t. an SOS semantics by embedding both into higher-order logic.
A strong (L) logicprogramming language ([14, 15]) is given by two subclasses of formulas (programs and goals) of the underlying logic L, provided that: firstly, any program P (viewed as a L-theory) has a canonical mo...
详细信息
ISBN:
(纸本)3540657193
A strong (L) logicprogramming language ([14, 15]) is given by two subclasses of formulas (programs and goals) of the underlying logic L, provided that: firstly, any program P (viewed as a L-theory) has a canonical model M-P which is initial in the category of all its C-models;secondly, the L-satisfaction of a goal G in Mp is equivalent to the L-derivability of G from P, and finally, there exists an effective (computable) proof-subcalculus of the L-calculus which works out for derivation of goals from programs. In this sense, Horn clauses constitute a strong (first-order) logicprogramming language. Following the methodology suggested in [15] for designing logicprogramming languages, an extension of Horn clauses should be made by extending its underlying first-order logic to a richer logic which supports a strong axiomatization of the extended logicprogramming language. A well-known approach for extending Horn clauses with embedded implications is the static scope programming language presented in [8]. In this paper we show that such language can be seen as a strong FOsuperset of logicprogramming language, where FOsuperset of is a very natural extension of first-order logic with intuitionistic implication. That is, we present a new characterization of the language in [8] which shows that Horn clauses extended with embedded implications, viewed as FOsuperset of theories, preserves all the attractive mathematical and computational properties that Horn clauses satisfy as first-order-theories.
Functional logicprogramming integrates the best features of modern functional and logic languages. The multi-paradigm declarative language Curry is an extension of Haskell which is intended to become a standard in th...
详细信息
ISBN:
(纸本)354066694X
Functional logicprogramming integrates the best features of modern functional and logic languages. The multi-paradigm declarative language Curry is an extension of Haskell which is intended to become a standard in the area. In this paper, we present UPV-Curry, an efficient and quite complete implementation of Curry based on a new, incremental definition of its basic evaluation mechanism. We compare UPV-Curry with already existing implementations of other Curry interpreters.
A knowledge-based system uses its database (also known as its "theory") to produce answers to the queries it receives. Unfortunately, these answers may be incorrect if the underlying theory is faulty. Standa...
详细信息
A knowledge-based system uses its database (also known as its "theory") to produce answers to the queries it receives. Unfortunately, these answers may be incorrect if the underlying theory is faulty. Standard "theory revision" systems use a given set of "labeled queries" (each a query paired with its correct answer) to transform the given theory, by adding and/or deleting either rules and/or antecedents, into a related theory that is as accurate as possible. After formally defining the theory revision task, this paper provides both sample and computational complexity bounds for this process. It first specifies the number of labeled queries necessary to identify a revised theory whose error is close to minimal with high probability. It then considers the computational complexity of finding this best theory, and proves that, unless P = NP, no polynomial-time algorithm can identify this optimal revision, even given the exact distribution of queries, except in certain simple situations. It also shows that, except in such simple situations, no polynomial-time algorithm can produce a theory whose error is even close to (i.e., within a particular polynomial factor of) optimal. The first (sample complexity) results suggest reasons why theory revision can be more effective than learning from scratch, while the second (computational complexity) results explain many aspects of the standard theory revision systems, including the practice of hill-climbing to a locally-optimal theory, based on a given set of labeled queries. (C) 1999 Elsevier Science B.V. All rights reserved.
This paper presents the first approximation method of the finite-failure set of a logic program by set-based analysis. In a dual view, the method yields a type analysis for programs with ongoing behaviors (perpetual p...
详细信息
ISBN:
(纸本)3540656995
This paper presents the first approximation method of the finite-failure set of a logic program by set-based analysis. In a dual view, the method yields a type analysis for programs with ongoing behaviors (perpetual processes). Our technical contributions are (1) the semantical characterization of finite failure of logic programs over infinite trees and (2) the design and soundness proof of the first set-based analysis of logic programs with the greatest-model semantics. Finally, we exhibit the connection between finite failure and the inevitability of the 'inconsistent-store' error in fair executions of concurrent constraint programs where no process suspends forever. This indicates a potential application to error diagnosis for concurrent constraint programs.
暂无评论