Tue 17 Jan 2023 16:30 - 17:00 at Arlington - Model Checking Chair(s): Eric Koskinen

Collective adaptive systems may be broadly defined as ensembles of autonomous agents, whose interaction may lead to the emergence of global features and patterns. Formal verification may provide strong guarantees about the emergence of these features, but may suffer from scalability issues caused by state space explosion. Compositional verification, whereby the state space of a system is generated by combining (an abstraction of) those of its components, has shown to be a promising countermeasure to the state space explosion problem. Therefore, in this work we apply these techniques to the problem of verifying collective adaptive systems with stigmergic interaction. Specifically, we automatically encode these systems into networks of LNT processes, apply a static value analysis to prune the state space of individual agents, and then reuse compositional verification procedures provided by the CADP toolbox. We demonstrate the effectiveness of our approach by verifying a collection of representative systems.

Tue 17 Jan

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

16:00 - 17:30
Model CheckingVMCAI at Arlington
Chair(s): Eric Koskinen Stevens Institute of Technology
16:00
15m
Talk
A Pragmatic Approach to Stateful Partial Order ReductionRecorded
VMCAI
Berk Cirisci IRIF, University Paris Diderot and CNRS, France, Constantin Enea Ecole Polytechnique / LIX / CNRS, Azadeh Farzan University of Toronto, Suha Orhun Mutluergil Sabanci University, Turkey
16:15
15m
Talk
StaticPersist : Compiler Support for PMEM ProgrammingRecorded
VMCAI
Sorav Bansal IIT Delhi and CompilerAI Labs
16:30
30m
Talk
Compositional Verification of Stigmergic Collective Systems
VMCAI
Luca Di Stefano University of Gothenburg, Sweden, Frederic Lang
17:00
30m
Talk
Synthesizing History and Prophecy Variables for Symbolic Model Checking
VMCAI
Cole Vick , Kenneth L. McMillan University of Texas at Austin