abstract:
Hoare monitors, invented by Brinch Hansen and Hoare in 1973, are widely used to safely handle concurrent programming in different languages ranging from C++11 to Tower, an EDSL developed by Galois as part of the High-Assurance Cyber Military Systems (HACMS) DARPA program. This talk will explain how basic safety properties are assured using Tower, and how it is possible to improve runtime efficiency and parallelism of Tower-generated C programs by releasing some constraints on the Hoare monitor model. Finally, some test results on SMACCMPilot, a high-assurance autopilot, will be presented.
bio:
Georges-Axel Jaloyan is a CS student at École Normale Supérieure in Paris. He is interning at Galois as part of his Master’s degree. He is interested in embedded systems security and safety-critical systems. He interned previously at NASA Langley Safety Critical Avionics Systems Branch.