POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Mon 20 Jan 2025 16:30 - 17:00 at Room 2 - Session 4

We present an approach for checking that Java programs correctly use libraries such as java.util.concurrent.locks for synchronizing concurrent tasks. Concretely, the article develops methods to check that the behaviour of a program is in accordance with a set of coding rules that govern the correct usage of the library. Here such coding rules are formalized as Prolog predicates that judge whether the history of interactions between program and library is permitted by the rule or not. The history of interactions is obtained by tracing the interactions between the program and the library when executing a representative test suite. The approach is evaluated in a case study where around two hundred independent monitor-based Java implementations of a common specification are analysed to check adherence to the concurrency coding rules.

This program is tentative and subject to change.

Mon 20 Jan

Displayed time zone: Mountain Time (US & Canada) change

16:00 - 17:30
Session 4PADL at Room 2
16:00
30m
Talk
MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs
PADL
Felipe Gorostiaga IMDEA Software Institute, Martin Ceresa IMDEA Software Institute, César Sánchez IMDEA Software Institute
16:30
30m
Talk
Checking Concurrency Coding Rules
PADL
Lars-Åke Fredlund Universidad Politécnica de Madrid, Ángel Herranz Universidad Politécnica de Madrid, Julio Mariño Universidad Politécnica de Madrid