@inproceedings{6035,
  abstract     = {We present JuliaReach, a toolbox for set-based reachability analysis of dynamical systems. JuliaReach consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JuliaReach can be applied to solve complex, large-scale problems.},
  author       = {Bogomolov, Sergiy and Forets, Marcelo and Frehse, Goran and Potomkin, Kostiantyn and Schilling, Christian},
  booktitle    = {Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control},
  isbn         = {9781450362825},
  keywords     = {reachability analysis, hybrid systems, lazy computation},
  location     = {Montreal, QC, Canada},
  pages        = {39--44},
  publisher    = {ACM},
  title        = {{JuliaReach: A toolbox for set-based reachability}},
  doi          = {10.1145/3302504.3311804},
  volume       = {22},
  year         = {2019},
}

@inproceedings{6428,
  abstract     = {Safety and security are major concerns in the development of Cyber-Physical Systems (CPS). Signal temporal logic (STL) was proposedas a language to specify and monitor the correctness of CPS relativeto formalized requirements. Incorporating STL into a developmentprocess enables designers to automatically monitor and diagnosetraces, compute robustness estimates based on requirements, andperform requirement falsification, leading to productivity gains inverification and validation activities; however, in its current formSTL is agnostic to the input/output classification of signals, andthis negatively impacts the relevance of the analysis results.In this paper we propose to make the interface explicit in theSTL language by introducing input/output signal declarations. Wethen define new measures of input vacuity and output robustnessthat better reflect the nature of the system and the specification in-tent. The resulting framework, which we call interface-aware signaltemporal logic (IA-STL), aids verification and validation activities.We demonstrate the benefits of IA-STL on several CPS analysisactivities: (1) robustness-driven sensitivity analysis, (2) falsificationand (3) fault localization. We describe an implementation of our en-hancement to STL and associated notions of robustness and vacuityin a prototype extension of Breach, a MATLAB®/Simulink®toolboxfor CPS verification and validation. We explore these methodologi-cal improvements and evaluate our results on two examples fromthe automotive domain: a benchmark powertrain control systemand a hydrogen fuel cell system.},
  author       = {Ferrere, Thomas and Nickovic, Dejan and Donzé, Alexandre and Ito, Hisahiro and Kapinski, James},
  booktitle    = {Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control},
  isbn         = {9781450362825},
  location     = {Montreal, Canada},
  pages        = {57--66},
  publisher    = {ACM},
  title        = {{Interface-aware signal temporal logic}},
  doi          = {10.1145/3302504.3311800},
  year         = {2019},
}