POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom

A significant transition is under way, regarding the role computers will be playing in a wide spectrum of application areas. I will present two work-in-progress projects that attempt to shed new light on this transition.

The first we term “The Human-or-Machine Issue”. Turing’s imitation game addresses the question of whether a machine can be labeled intelligent. We explore a related, yet quite different, challenge: in everyday interactions with an agent, how will knowing whether the agent is human or machine affect that interaction? In contrast to Turing’s test, this is not a thought experiment, but is directly relevant to human behavior, human-machine interaction and also system development. Exploring the issue now is useful even if machines will end up not attempting to disguise themselves as humans, which might become the case because they cannot do so well enough, because doing so will not be that helpful, because machines exceed human capabilities, or because regulation forbids it.

In the second project, we propose a systematic programming methodology that consists of three main components: (1) a modular incremental specification approach (specifically, scenario-based programming); (2) a powerful, albeit error-prone, AI-based software development assistant; and (3) systematic iterative articulation of requirements and system properties, amid testing and verification. The preliminary results we have obtained show that one can indeed use an AI chatbot as an integral part of an interactive development method, during which one constantly verifies each new artifact contributed by the chatbot in the context of the evolving system.

While seemingly quite diverse, both projects have human-machine interaction at their heart, and bring in their wake common meta-concepts, such as trust and validity. What, for example, are the effects of the presence or absence of trust in such interactions, and how does one ensure that the interaction contributes to achieving one’s goals, even when the motives of the other party or the quality of its contributions are unclear?

In addition, the kinds of interactions we discuss have a strong dynamic nature: multi-step interaction on requirements elicitation, for example, is not just a search for something that should have been specified in full earlier. Rather, it is often a constructive process of building new knowledge, acquiring new understanding, and demarcating explicit boundaries and exceptions that are often absent from even the most rigorous definitions.

Research joint with Assaf Marron, Guy Katz and Smadar Szekely.

Mon 15 Jan

Displayed time zone: London change

09:00 - 10:30
Session 1: Openning, Keynote, SAT, SMT and Automated ReasoningVMCAI at Marconi Room
Chair(s): Rayna Dimitrova CISPA Helmholtz Center for Information Security
09:00
5m
Day opening
Opening
VMCAI

09:05
60m
Keynote
Two Projects on Human Interaction with AI
VMCAI
David Harel Weizmann Institute of Science, Israel
10:05
20m
Talk
Interpolation and Quantifiers in Ortholattices
VMCAI
Sankalp Gambhir Ecole Polytechnique Federale de Lausanne (EPFL), Simon Guilloud École Polytechnique Fédérale de Lausanne, Viktor Kunčak EPFL, Switzerland