You are here

2004

  1. F. Roelofsen; L. Serafini; A. Cimatti,
    Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems,
    Proceedings of 16th Eureopean Conference on Artificial Intelligence,
    2004
    , pp. 58-
    62
    , (ECAI'2004,
    Valencia, Spain,
    22/08/2004-27/08/2004)
  2. Marco Bozzano; Alessandro Cimatti; Gabriele Colombini; Veselin Kirov; Roberto Sebastiani,
    The MathSAT solver -- a progress report,
    Proceeding of 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning,
    2004
    , (PDPAR,
    University College Cork, Ireland,
    05/07/2004)
  3. Marco Pistore; Marco Roveri; Paolo Busetta,
    Requirements-Driven Verification of Web Services,
    Proceedings of 1st Int. Workshop on Web Services and Formal Methods,
    2004
    , (WS-FM,
    Pisa, Italu,
    23-24/02/2004)
  4. Roberto Sebastiani; Eli Singerman; Stefano Tonetta; Moshe Vardi,
    Proceedings of the 16th Int. Conference on Computer-Aided Verification,
    Springer,
    vol.3114,
    2004
    , pp. 301-
    305
    , (CAV,
    Boston, MA, USA,
    13-17/07/2004)
  5. M. Bozzano; A. Cimatti; G. Colombini; V. Kirov; R. Sebastiani,
    The MAthSAT Solver. A progress report,
    Many problems of practical relevance are conveniently expressed as boolean combinations of propositional variables and mathematical constraints. The development of decision procedures able to check the satisfiability of such formulas is therefore being devoted an increasing interest.
    The MathSat family of deciders is based on the extension of a DPLL propositional satisfiability procedure, used as an assignment enumerator. MathSat pioneers a lazy and layered approach, where propositional reasoning is tightly integrated with solvers of increasing expressive power (e.g. to reason about equality and linear arithmetic) in such a way that ``more expensive'' layers are called less frequently.
    In this paper, we show the advances in the development of MathSat. We discuss the implications related to the use of Minisat, a new-generation propositional SAT solver; the role of an incremental mathematical reasoner; the role of static learning; and the extension to integer variables. We show that the new version of MathSat is significantly more efficient than the previous one
    ,
    2004
  6. Marco Bozzano; R. Bruttomesso; A. Cimatti; R. Sebastiani,
    The MathSAT Solver - a comparative evaluation,
    Many problems of practical relevance are conveniently expressed as boolean combinations of propositional variables and mathematical constraints. The development of decision procedures able to check the satisfiability of such formulas is therefore being devoted an increasing interest. The MathSat family of deciders is based on the extension of a DPLL propositional satisfiability procedure, used as an assignment enumerator. MathSat pioneers a lazy and layered approach, where propositional reasoning is tightly integrated with solvers of increasing expressive power (e.g. to reason about equality and linear arithmetic) in such a way that "more expensive" layers are called less frequently.
    In this paper, we discuss the advances in the development of MathSat. In particular, the current version of the tool is built on minisat, a new-generation propositional SAT solver, and Cassowary, an incremental mathematical reasoner, and it incorporates support for integer variables. We compare the performance of MathSat with CVCL and show that MathSat is significantly more efficient on a set of benchmarks related to word-level verification
    ,
    2004
  7. P. Traverso; M. Pistore; M. Roveri; A. Marconi; R. Kazhamiakin; P. Lucchese; P. Busetta; P. Bertoli,
    Supporting the Negotiation between Global and Local Business Requirements in Service oriented Development,
    The development of service oriented applications very often needs to address the problem of satisfying two conflicting kinds of business needs: global business requirements, i.e., the regulations that dictate the rules of engagement between different organizations, and local business requirements, i.e., the rules local to each involved partner which derive from its internal business needs. In this paper, we propose a development process where both global and local service requirements, as well as their behaviors, are incrementally agreed among partners and built through negotiation steps. The development process is supported by the explicit definition of both global and local requirements at different levels of abstraction. We express requirements in a language with a clear semantics, and which allows for explicit links to executable business processes, e.g., written in BPEL4WS. This development process opens up the possibility to adopt a variety of supporting techniques. In particular, automated verification is used to detect design or implementation problems. Automated synthesis of executable business processes allows for a speed up in the development process and reduces development effort. Finally, execution monitoring is able to detect run-time problems with respect to specified requirements,
    2004

Pages