ARCH15: Volume Information
Volume:Goran Frehse and Matthias Althoff (editors).
ARCH14-15. 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems

Volume Information

Title:ARCH14-15. 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems
Editors:Goran Frehse and Matthias Althoff
Series:EPiC Series in Computing
Publication date:December 17, 2015


Victor Gan, Guy Dumont and Ian MitchellBenchmark Problem: A PK/PD Model and Safety Constraints for Anesthesia Delivery1-8
Hongxu Chen, Sayan Mitra and Guangyu TianMotor-Transmission Drive System: a Benchmark Example for Safety Verification9-18
Luan Viet Nguyen and Taylor T JohnsonBenchmark: DC-to-DC Switched-Mode Power Converters (Buck Converters, Boost Converters, and Buck-Boost Converters)19-24
Bardh Hoxha, Houssam Abbas and Georgios FainekosBenchmarks for Temporal Logic Requirements for Automotive Systems25-30
Thomas Heinz, Jens Oehlerking and Matthias WoehrleBenchmark: Reachability on a model with holes31-36
Ibtissem Ben Makhlouf and Stefan KowalewskiNetworked Cooperative Platoon of Vehicles for Testing Methods and Verification Tools37-42
Luca Parolini, Simone Schuler and Adolfo AntaBenchmark problem: an air brake model for trains43-48
Thomas Strathmann and Jens OehlerkingVerifying Properties of an Electro-Mechanical Braking System49-56
A. E. C. Da CunhaBenchmark: Quadrotor Attitude Control57-72
Stanley Bak, Sergiy Bogomolov, Marius Greitschus and Taylor T JohnsonBenchmark Generator for Stratified Controllers of Tank Networks73-79
Hendrik Roehm, Rainer Gmehlich, Thomas Heinz, Jens Oehlerking and Matthias WoehrleIndustrial Examples of Formal Specifications for Test Case Generation80-88
Hoang-Dung Tran, Luan Viet Nguyen and Taylor T JohnsonBenchmark: A Nonlinear Reachability Analysis Test Set from Numerical Analysis89-97
Jyotirmoy Deshmukh, Hisahiro Ito, Xiaoqing Jin, James Kapinski, Ken Butts, Juergen Gerhard, Behzad Samadi, Kevin Walker and Yuzhen XiePiecewise-Affine Approximations for a Powertrain Control Verification Benchmark98-112
Bardh Hoxha, Houssam Abbas and Georgios FainekosUsing S-TaLiRo on Industrial Size Automotive Models113-119
Matthias AlthoffAn Introduction to CORA 2015120-151
Xin Chen, Sriram Sankaranarayanan and Erika AbrahamFlow* 1.2: More Effective to Play with Hybrid Systems152-159
Alexandre Donzé and Vasumathi RamanBluSTL: Controller Synthesis from Signal Temporal Logic Specifications160-168
Ibtissem Ben Makhlouf and Stefan KowalewskiOptimizing Safe Control of a Networked Platoon of Trucks Using Reachability169-179
Fabian ImmlerTool Presentation: Isabelle/HOL for Reachability Analysis of Continuous Systems180-187
Kyungmin Bae, Soonho Kong and Sicun GaoSMT Encoding of Hybrid Systems in dReal188-195
Stefano Minopoli and Goran FrehseRunning SpaceEx on the ARCH14 Benchmarks196-206
Chuchu Fan, Parasara Sridhar Duggirala, Sayan Mitra and Mahesh ViswanathanProgress on Powertrain Verification Challenge with C2E2207-212


Academic5, affine arithmetic, algorithmic verification, Anesthesia, attitude control, Automotive6, benchmark11, BluSTL, C2E2, circuits, continuous systems, control8, CORA, Discrepancy Functions, dReach, dReal, Educational, experience report, falsification2, Flow*3, formal specifications, generator, H2/Hinf control, HOL, hybrid automata3, hybrid systems6, hypnosis, Hyst, Industrial6, interactive theorem proving, Isabelle, iSAT-ODE, Maple, MATLAB4, Mixed Integer Linear Programming, Model Predictive Control, Networked Systems, nonlinear differential algebraic equations, Nonlinear ordinary differential equations, ordinary differential equations, pharmacodynamics, pharmacokinetics, piecewise affine, PKPD, Platoon, powertrain, Powertrain control, Propofol, Python, Quadrotor, reachability6, Rigorous Numerics, S-Taliro2, safety7, set-representations, Signal Temporal Logic, simulation, Simulink4, SMT, SpaceEx4, Stateflow4, Support Functions, switched systems, synthesis, tank, Taylor model, temporal logic2, test case generation, tools8, train control, verification10, zonotopes.