<< back

ReaVer - Reactive System Verifier


ReaVer is a tool framework for safety verification of discrete and hybrid systems specified by logico-numerical data-flow languages, like Lustre, Lucid Synchrone or Zelus. It provides time-unbounded analysis based on abstract interpretation techniques.

It features partitioning techniques and logico-numerical analysis methods based on Kleene iteration with widening and descending iterations, abstract acceleration, max-strategy iteration, and relational abstractions; logico-numerical product and power domains (based on the APRON and BddApron domain libraries) with convex polyhedra, octagons, intervals, and template polyhedra; and frontends for the hybrid NBac format, Lustre via lus2nbac, and Zelus/Lucid Synchrone.

News
Tool
Documentation and benchmarks
Publications
  • Peter Schrammel. Logico-Numerical Verification Methods for Discrete and Hybrid Systems. PhD Thesis, University of Grenoble, France. [bibtex] [pdf]
(Logico-numerical) abstract acceleration:
  • Peter Schrammel and Pavle Subotic. Logico-Numerical Max-Strategy Iteration. In Verification, Model Checking and Abstract Interpretation, VMCAI'13. Vol. 7737 of LNCS, pp. 414-433, 2013. [bibtex] [link]
  • Peter Schrammel and Bertrand Jeannet. Applying Abstract Acceleration to (Co-)Reachability Analysis of Reactive Programs. Journal of Symbolic Computation, 47(12):1512-1532, 2012. [bibtex] [link]
  • Peter Schrammel and Bertrand Jeannet. Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs. In Static Analysis, SAS'11. Vol. 6887 of LNCS, pp. 233-248, Springer, 2011. [bibtex] [link]
  • Peter Schrammel and Bertrand Jeannet. Extending Abstract Acceleration to Data-Flow Programs with Numerical Inputs. In Numerical and Symbolic Abstract Domains, NSAD'10. Vol. 267 of ENTCS, pp. 101-114, Elsevier, 2010. [bibtex] [link]
Logico-numerical hybrid automata:
  • Peter Schrammel and Bertrand Jeannet. From Hybrid Data-Flow Languages to Hybrid Automata: A Complete Translation. In Hybrid Systems: Computation and Control, HSCC'12. pp. 167-176, ACM, 2012. [bibtex] [link]
action d'envergure Synchronics