SpaceEx: Scalable Verification of Hybrid Systems

By Goran Frehse, C. J. Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, T. Dang, Oded Maler. International Conference on Computer Aided Verification, 2011

987 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Hardware and Architecture, Software

View Paper: https://www.semanticscholar.org/paper/4888eeab485e485786fc5125b13f91dc5c2fba1a

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

In Hardware and Architecture

In Software

Citations in the corpus

Hamilton-Jacobi reachability: A brief overview and recent advances (2017, methodology): “Numerous tools such as SpaceEx [24], Flow* [25], CORA [26], C2E2 [27], [28], and dReach [29] have been developed for this purpose; the authors in [30] present a tutorial on combining different tools for hybrid systems veriﬁcation.”
A Roadmap Toward the Resilient Internet of Things for Cyber-Physical Systems (2018, neutral): “Recent surveys [37] [32] [46] [28] [49] [50] [51] Additional [52] [36] [53] [37] [54] [37] [55] [56] [57] [58] [59] Exemplary [60] [61] [62] [63] [64] [65] [66] [67] [68] [69] [70] [71] [72] [73] [74] [75] [76] [77] [78] [79] [80] [81] [82] [83] [84] [85] [86] [87] [88] [89] [90] [91] [92] [93] [94]”
Formal verification of hybrid systems (2011, methodology): “Representation using zonotopes and support functions [22,26] has so far resulted in the most scalable approach for the analysis of linear hybrid systems, leading to the tool SpaceEx that is able to analyze, for instance, a complex 28-dimensional helicopter controller [20].”
Online Verification of Automated Road Vehicles Using Reachability Analysis (2014, background): “In other work s, the relative error rather than the absolute error is control led [54], [55].”
Flow*: An Analyzer for Non-linear Hybrid Systems (2013, methodology): “The verification techniques developed for hybrid systems over the last few decades have resulted in many tools for linear hybrid systems analysis including HyTech, Checkmate, d/dt, Ariadne, HySAT/iSAT, RealPaver, PHAVer, SpaceEx [7].”
Planning as Model Checking in Hybrid Domains (2014, methodology): “As a case study, we apply our translation with the SpaceEx model checker (Frehse et al. 2011), which is considered as a state-of-the art tool in the area of hybrid systems model checking.”
Set Propagation Techniques for Reachability Analysis (2021, neutral): “1: ellipsoids [57, 58], polytopes [59, 60], zonotopes [61, 62] or support functions [63, 64].”
Cyber–Physical Systems: A Perspective at the Centennial (2012, methodology): “Some examples are UPPAAL [118], a verification tool for real-time systems based on timed automata, HyTech [99] and PHAVer [119] for LHA, SpaceEx [120] which is based on the LeGuernic-Girard (LGG) algorithm [121] that can efficiently”