Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF

DOI10.1007/978-3-662-54577-5_4zbMath1452.68116arXiv1801.08718OpenAlexW3104841382WikidataQ62041073 ScholiaQ62041073MaRDI QIDQ3303890

Alberto Griggio, Roberto Sebastiani, Marco Roveri, Ahmed Irfan, Alessandro Cimatti

Publication date: 5 August 2020

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1801.08718

zbMATH Keywords

abstraction refinementuninterpreted functionsinvariant checkinglinear real arithmetic (LRA)safety benchmark

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (4)

Interpolation and model checking for nonlinear arithmetic ⋮ Lattice-based refinement in bounded model checking ⋮ Levelwise construction of a single cylindrical algebraic cell ⋮ \textsc{OptiMathSAT}: a tool for optimization modulo theories

Uses Software

• MiniSat
• Yices
• z3
• dReal
• CalCS
• nuXmv
• Spacer
• PySMT
• HYST
• HyComp
• dReach
• CTIGAR
• iSAT

Cites Work

• Unnamed Item
• SMT-based model checking for recursive programs
• Infinite-state invariant checking with IC3 and predicate abstraction
• Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
• Generalized Property Directed Reachability
• Solving Non-linear Arithmetic
• HYST
• Craig Interpolation in the Presence of Non-linear Constraints
• dReal: An SMT Solver for Nonlinear Theories over the Reals
• Computer Aided Verification

This page was built for publication: Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF