Four papers by IMDEA Software Institute researchers have been accepted for publication in the proceedings of the 27th International Conference on Computer Aided Verification, a top-ranked conference in this important field, held this year in San Francisco, CA. These four papers are among 68 selected for publication from over 250 submissions.
IMDEA Software Institute faculty member César Sánchez has a paper on model checking “hyperproperties”, together with Bernd Finkbeiner and Markus Rabe from IMDEA Software Institute. Their paper characterizes the precise complexity of the model checking problem for hyperproperties, and shows how to leverage existing state-of-the-art model checking tools to handle hyperproperty specifications, with applications to security, symmetry, and coding theory.
IMDEA Software Institute faculty member Boris Köpf has a paper together with Klaus von Gleissenthall ((IMDEA Software Institute) and Andrey Rybalchenko (IMDEA Software Institute) on verifying quantitative program properties, such as bounds on resource usage or information leaks. The core technical novelty is an SMT-based algorithm for synthesizing interpolants with cardinality constraints that relies on the theory of counting integer points in symbolic polytopes.
IMDEA Software Institute faculty member Michael Emmi’s contribution reports on the development of a tool for uncovering concurrency bugs in Android apps, a joint work with Burcu Kulahcioglu Ozkan and Serdar Tasiran of Koç University in Turkey.
IMDEA Software Institute faculty member Pierre Ganty has a paper on the automated verification of shared-memory asynchronous systems together with A. Durand-Gasselin, J. Esparza from IMDEA Software Institute and R. Majumdar from IMDEA Software Institute. Their work classifies verification problems for liveness properties in shared-memory asynchronous systems from a computational point of view. These systems are characterized by a leader process and arbitrarily-many anonymous and identical contributors. Processes communicate through a shared, bounded-value register.
Find more information on the conference website.
