Item request has been placed! ×
Item request cannot be made. ×
loading  Processing Request

A Decision Procedure for (Co)datatypes in SMT Solvers

Item request has been placed! ×
Item request cannot be made. ×
loading   Processing Request
اقرأ أكثر حفظ في قائمتي
  • معلومة اضافية
    • Contributors:
      Ecole Polytechnique Fédérale de Lausanne (EPFL); Modeling and Verification of Distributed Algorithms and Systems (VERIDIS); Max-Planck-Institut für Informatik (MPII); Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM); Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA); Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA); Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS); The second author’s research was partially supported by the Deutsche Forschungsgemeinschaft project “Den Hammer härten” (grant NI 491/14-1) and the Inria technological development action “Contre-exemples Utilisables par Isabelle et Coq” (CUIC).
    • بيانات النشر:
      HAL CCSD
    • الموضوع:
      2015
    • Collection:
      Université de Lorraine: HAL
    • الموضوع:
      Berlin; Germany
    • نبذة مختصرة :
      International audience ; We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyclic values. The procedure decides universal problems and is composable via the Nelson–Oppen method. It has been implemented in CVC4, a state-of-the-art SMT solver. An evaluation based on problems generated from theories developed with Isabelle demonstrates the potential of the procedure.
    • Relation:
      hal-01212585; https://inria.hal.science/hal-01212585; https://inria.hal.science/hal-01212585/document; https://inria.hal.science/hal-01212585/file/conf.pdf
    • الرقم المعرف:
      10.1007/978-3-319-21401-6_13
    • Rights:
      info:eu-repo/semantics/OpenAccess
    • الرقم المعرف:
      edsbas.C6E15132