Authoring and verification of human-robot interactions

We developed a graphical authoring environment, RoVer, that enables users to program social robots, and provides feedback on whether or not the robots will violate social norms. Designers drag and drop robot behaviors into the editing environment to create an interaction flow, which RoVer converts into an executable program. Given a set of social norms that the robot needs to abide by, RoVer uses techniques from formal verification to perform real-time checking of designer-created programs against each social norm. If RoVer detects that a designer-created program will violate a social norm, the social norm is flagged and presented in plain English. We evaluated the effect 0f formal verification on the design process, and found that designers are more able to identify and understand social norm violations that exist within their programs. We presented our results at the 2018 ACM User Interface Software and Technology Symposium in Berlin, Germany, and won best paper award for our work.

The Team

  • David Porfirio

    Postdoctoral Fellow, Naval Research Laboratory

  • Allison Sauppé

    Associate Professor, UW-La Crosse

  • Aws Albarghouthi

    Associate Professor

  • Bilge Mutlu

    Sheldon B. and Marianne S. Lubar Professor, Computer Science


  • National Science Foundation

The Robot