JavaScript is disabled for your browser. Some features of this site may not work without it.
    View Item 
    •   OpenBU
    • College of Arts and Sciences
    • Computer Science
    • CAS: Computer Science: Technical Reports
    • View Item
    •   OpenBU
    • College of Arts and Sciences
    • Computer Science
    • CAS: Computer Science: Technical Reports
    • View Item

    Towards lightweight integration of SMT solvers

    Thumbnail
    Download/View
    2012-017-smt-i...pdf (198.4Kb)
    Date Issued
    2012-12-10
    Author
    Lapets, Andrei
    Mizraei, Saber
    Share to FacebookShare to TwitterShare by Email
    Export Citation
    Download to BibTex
    Download to EndNote/RefMan (RIS)
    Metadata
    Show full item record
    Permanent Link
    https://hdl.handle.net/2144/11405
    Citation
    Lapets, Andrei; Mizraei, Saber. Towards Lightweight Integration of SMT Solvers, Technical Report BUCS-TR-2012-017, Computer Science Department, Boston University, December 10, 2012. [Available from: http://hdl.handle.net/2144/11405]
    Abstract
    A large variety of SMT techniques and associated solvers have been developed by the formal modelling and verification communities. For a particular application domain, each technique has its own unique set of advantages and limitations. Within the context of a particular application domain (characterized by a particular set of possible logical formulas), the fitness of a technique can be characterized along multiple dimensions: expressiveness, soundness, completeness, response time, computational cost, and others. Furthermore, certain application domains may require that multiple techniques be used in concert in order to address the particular set of formulas that must be supported. We present a prototype lightweight integrated environment that incorporates four different cloud-hosted SMT solvers behind a single web-based interface: CVC3, Alt-Ergo, Yices, and Z3. Formulas submitted using a common logical syntax are translated into representations suitable for each of the underlying SMT solvers. We discuss the characteristics of each of the SMT solvers, in part by presenting the target syntaxes of the translations (including what outputs the solvers can produce and how this relates to their completeness with respect to the common syntax). We then discuss future directions, including the automated characterization of SMT solvers integrated into the infrastructure in terms of expressiveness, completeness, and response time.
    Collections
    • CAS: Computer Science: Technical Reports [584]

    Contact Us | Send Feedback | Help
     

     

    Browse

    All of OpenBUCommunities & CollectionsIssue DateAuthorsTitlesSubjectsThis CollectionIssue DateAuthorsTitlesSubjects

    Deposit Materials

    LoginNon-BU Registration

    Statistics

    Most Popular ItemsStatistics by CountryMost Popular Authors

    Contact Us | Send Feedback | Help