SPLAT! How to Avoid Bugs while Driving on the Highway

Abstract. A bug on your windshield does little damage, but a bug in the software that controls your engine, brakes or steering is catastrophic. Driver assistance technologies, like adaptive cruise control and automatic braking protocols, have the potential to increase the efficiency of crowded roads, but more compelling is their capacity for reducing the number of accidents and fatalities resulting from driver error. Yet, increased depen- dence on this next-generation technology is wise only when its reliability has been ensured and regulated.

Our methods can't protect your windshield from insects as you cruise down the highway, but with continued research we can remove the dan- gerous software bugs in safety-critical systems that testing and model checking overlook.

References

1. Ar echiga, N., Loos, S.M., Platzer, A., Krogh, B.H.: Using theorem provers to guar- antee closed-loop system properties. In: Tilbury, D. (ed.) ACC (2012)

2. Loos, S.M., Platzer, A.: Safe intersections: At the crossing of hybrid systems and verification. In: Yi, K. (ed.) ITSC. pp. 1181-1186. Springer (2011)

3. Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: Hybrid, distributed, and now formally verified. In: Butler, M., Schulte, W. (eds.) FM. LNCS, vol. 6664, pp. 42-56. Springer (2011)

4. Mitsch, S., Loos, S.M., Platzer, A.: Towards formal verification of freeway traffic control. In: Lu, C. (ed.) ICCPS. pp. 171-180. IEEE (2012)

5. Platzer, A.: Quantified differential dynamic logic for distributed hybrid systems. In: Dawar, A., Veith, H. (eds.) CSL. LNCS, vol. 6247, pp. 469-483. Springer (2010)

6. Platzer, A.: Quantified differential invariants. In: Frazzoli, E., Grosu, R. (eds.)

   HSCC. pp. 63-72. ACM (2011)

7. Platzer, A.: A complete axiomatization of quantified differential dynamic logic for

   distributed hybrid systems. Logical Methods in Computer Science (2012), special

   issue for selected papers from CSL'10

8. Platzer, A.: Logics of dynamical systems. In: LICS. pp. 13-24. IEEE Computer

   Society (2012)

9. Rajhans, A., Bhave, A., Loos, S.M., Krogh, B.H., Platzer, A., Garlan, D.: Using

   parameters in architectural views to support heterogeneous design and verification.

   In: CDC. pp. 2705-2710 (2011)

10. Renshaw, D.W., Loos, S.M., Platzer, A.: Distributed theorem proving for dis-

    tributed hybrid systems. In: Qin, S., Qiu, Z. (eds.) ICFEM. LNCS, vol. 6991, pp. 356-371. Springer (2011)

Award ID: 0931985