Serwis Infona wykorzystuje pliki cookies (ciasteczka). Są to wartości tekstowe, zapamiętywane przez przeglądarkę na urządzeniu użytkownika. Nasz serwis ma dostęp do tych wartości oraz wykorzystuje je do zapamiętania danych dotyczących użytkownika, takich jak np. ustawienia (typu widok ekranu, wybór języka interfejsu), zapamiętanie zalogowania. Korzystanie z serwisu Infona oznacza zgodę na zapis informacji i ich wykorzystanie dla celów korzytania z serwisu. Więcej informacji można znaleźć w Polityce prywatności oraz Regulaminie serwisu. Zamknięcie tego okienka potwierdza zapoznanie się z informacją o plikach cookies, akceptację polityki prywatności i regulaminu oraz sposobu wykorzystywania plików cookies w serwisie. Możesz zmienić ustawienia obsługi cookies w swojej przeglądarce.
The talk describes some of the formal foundations of Juno- 2, a constraint-based graphical illustrator implemented by Allan Heydon and Greg Nelson and available over the web in source form. The first idea underlying Juno-2 is that constraint-based programming is obtained from ordinary imperative programming not by adding a feature but by subtracting a restriction: specifically by dropping the...
For the recently developed specification language CASL, there exist two different kinds of proof support: While HOL-CASL has its strength in proofs about specifications in-the-small, Maya has been designed for management of proofs in (CASL) specifications in-the-large, within an evolutionary formal software development process involving changes of specifications. In this work, we discuss our integration...
This paper argues that the core of modularity problems is an understanding of how individual components of a large system interact with each other, and that this interaction can be described by a layerstructure. We propose a uniform treatment of layers based upon the concept of a monad. The combination of different systems can be described by the coproduct of monads. Concretely,...
We are interested in investigating the confluence properties of cooperating constraint solvers. To this end, we model solvers as reductions that transform constraint networks, we define the notion of insensitivity to a superset relation, and show that, if each solver of a given set of solvers is insensitive to the same terminating superset relation, then any combination of these solvers is confluent...
Symbolic model checking is a very successful formal verification technique, classically based on Binary Decision Diagrams (BDDs). Recently, propositional satisfiability (SAT) techniques have been proposed as a computational basis for symbolic model checking, and proved to be an effective alternative to BDD-based techniques. In this paper we show how BDD-based and SAT-based techniques have been effectively...
Composite Symbolic Library is a symbolic manipulator for model checking systems with heterogeneous data types. Our current implementation uses two basic symbolic representations: BDDs for boolean and enumerated variables, and polyhedra for (unbounded) integers. These basic representations are imported to the Composite Symbolic Library using a common interface and are combined using a disjunctive composite...
We present a fully-automatic method for checking safetyproperties of parameterized synchronous systems based on a backwardreachability procedure working over real arithmetics. We consider here concurrent systems consisting of many identical (finite-state) processes and one monitor where processes may react non-deterministically to the messages sent by the monitor. This type of...
A rewrite rule based framework for combining decision procedures for universally quantified theories is proposed. It builds on the key ideas of Shostak's combination approach. A distinctive feature of the proposed framework is that its soundness and completeness can be easily established. Furthermore, the framework has the desired property of being efficient (by avoiding duplication of equality reasoning...
We present a decision procedure for a constraint language combining stratified sets of ur-elements with integers in the presence of a cardinality operator. Our decision procedure is an extension of the Nelson-Oppen combination method specifically tailored to the combination domain of sets, integers, and ur-elements.
The solving engines of most of constraint programming systems use interval-based consistency techniques to process nonlinear systems over the reals. However, few symbolic-interval cooperative solvers are implemented. The challenge is twofold: control of the amount of symbolic computations, and prediction of the accuracy of interval computations over transformed systems. In this paper, we introduce...
Consider the problem of determining whether a quantifier-free formula ϕ is satisfiable in some first-order theory T . Shostak#x2019;s algorithm decides this problem for a certain class of theories with both interpreted and uninterpreted function symbols. We present two new algorithms based on Shostak#x2019;s method. The first is a simple subset of Shostak's algorithm for the same class of theories...
The goal of this paper is to provide a strong interaction between constraint programming and relational DBMSs. To this end we propose extensions of standard query languages such as relational algebra (RA) and SQL, by adding constraint solving capabilities to them. In particular, we propose non-deterministic extensions of both languages, which are specially suited for combinatorial problems. Non-determinism...
We consider the language obtained by mixing the model of the regions and the propositional linear temporal logic. In particular, we propose alternative languages where the model of the regions is replaced by different forms of qualitative spatial or temporal reasoning. In these languages, qualitative formulas describe the movement and the relative positions of spatial or temporal entities in some...
Constraint Logic Programming languages on Finite Domains CLP(FD) provide a declarative framework for dealing with problems in Artificial Intelligence (AI). However, in many applications, domains are not known at the beginning of the computation and must be computed. The domain computation can be time-consuming, since elements can be retrieved through an expensive acquisition process from the outer...
Constraint reasoning finds more and more applications. The rule-based concurrent programming language Constraint Handling Rules (CHR) was introduced to ease the development of constraint reasoners. Currently several CHR libraries exist in languages such as Prolog, Haskell and Java, worldwide more than 50 projects use CHR. CHR and dozens of its constraint reasoners/solvers can be used online via the...
Prosper is a recently-completed ESPRIT Framework IV research project that investigated software architectures for component-based, embedded formal verification tools. The aim of the project was to make mechanized formal analysis more accessible in practice by providing a framework for integrating formal proof tools inside other software applications. This paper is an extended abstract of an invited...
We introduce two forms of calculi that integrate constraint solving with functional programming. These are the Unrestricted, and the Restricted, Constraint-Lambda Calculi. Unlike previous attempts at combining constraint solving with lambda calculus, these are conservative extensions of traditional lambda calculi in terms of both term reduction and their denotational semantics. We establish a limited...
We introduce a framework for presenting non-classical logics in a modular and uniform way as labelled natural deduction systems. The use of algebras of truth-values as the labelling algebras of our systems allows us to give generalized systems for multiple-valued logics. More specifically, our framework generalizes previous work where labels represent worlds in the underlying Kripke structure: since...
This work is focused on the study of temporal × modal logics. These logics have been traditionally used in several fields such as causation, the theory of actions, conditionals and others. In this paper we study the representation of properties of functions of interest because of their possible computational interpretations. The semantics is exposed in an algebraic style, and the definability of the...
Podaj zakres dat dla filtrowania wyświetlonych wyników. Możesz podać datę początkową, końcową lub obie daty. Daty możesz wpisać ręcznie lub wybrać za pomocą kalendarza.