Reachability Modulo Theory Library | Zendy

Francesco Alberti | Zendy; Roberto Bruttomesso | Zendy; Silvio Ghilardi | Zendy; Silvio Ranise | Zendy; Natasha Sharygina | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Reachability Modulo Theory Library

Author(s) -

Francesco Alberti,

Roberto Bruttomesso,

Silvio Ghilardi,

Silvio Ranise,

Natasha Sharygina

Publication year - 2018

Publication title -

epic series in computing

Language(s) - English

Resource type - Conference proceedings

ISSN - 2398-7340

DOI - 10.29007/f3rp

Subject(s) - reachability , computer science , modulo , programming language , transition system , formal verification , theoretical computer science , state (computer science) , mathematics , discrete mathematics

Reachability analysis of infinite-state systems plays a central role in many verification tasks. In the last decade, SMT-Solvers have been exploited within many verification tools to discharge proof obligations arising from reachability analysis. Despite this, as of today there is no standard language to deal with transition systems specified in the SMT-LIB format. This paper is a first proposal for a new SMT-based verification language that is suitable for defining transition systems and safety properties.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research