ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Mon 8 Apr 2019 14:00 - 14:30 at SUN I - Verification and Analysis Chair(s): Dirk Beyer

We present Linear Controller Verifier (LCV), a tool to verify that a controller implementation code correctly implements a linear controller model. The use of unverified code generator/transformer in the controller development may result in introducing unintended bugs in the controller implementation. Given a Simulink block diagram model and a C code implementation, LCV verifies an input-output equivalence between them. A real-world case study with the controller of a quadrotor system is demonstrated.

Mon 8 Apr

tacas-2019-papers
14:00 - 16:00: TACAS 2019 - Verification and Analysis at SUN I
Chair(s): Dirk BeyerLMU Munich
tacas-2019-papers14:00 - 14:30
Talk
Junkil ParkUniversity of Pennsylvania, Miroslav PajicDuke University, Oleg SokolskyUniversity of Pennsylvania, USA, Insup Lee
Link to publication
tacas-2019-papers14:30 - 15:00
Talk
Maria ChristakisMPI-SWS, Matthias HeizmannUniversity of Freiburg, Muhammad Numair MansurMax Planck Institute for Software Systems (MPI-SWS), Christian SchillingIST Austria, Valentin WüstholzConsenSys Diligence
Link to publication
tacas-2019-papers15:00 - 15:30
Talk
Benjamin BispingTechnische Universität Berlin, Uwe Nestmann
Link to publication
tacas-2019-papers15:30 - 16:00
Talk
Christian SternagelUniversity of Innsbruck, Austria, Akihisa Yamada
Link to publication