POPL 2017 (series) / VMCAI 2017 (series) / VMCAI /
Reduction of Workflow Nets for Generalised Soundness Verification
Mon 16 Jan 2017 14:30 - 15:00 at Amphitheater 44 - Model-checking and bug finding Chair(s): Andreas Podelski
This paper proposes a reduction method to verify the generalised soundness of large workflows described as workflow nets–a suited class of Petri nets. The proposed static analysis method is based on the application of six novel reduction transformations that transform a workflow net into a smaller one while preserving generalised soundness. The soundness of the method is proved. As practical contributions, this paper presents convincing experimental results obtained using a dedicated tool, developed to validate and demonstrate the effectiveness, efficiency and scalability of this method over a large set of industrial workflow nets.
Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:30 | Model-checking and bug findingVMCAI at Amphitheater 44 Chair(s): Andreas Podelski University of Freiburg, Germany | ||
14:00 30mTalk | Effective Bug Finding in C Programs with Shape and Effect Abstraction VMCAI Iago Abal IT University of Copenhagen, Claus Brabrand IT University of Copenhagen, Denmark, Andrzej Wąsowski IT University of Copenhagen, Denmark | ||
14:30 30mTalk | Reduction of Workflow Nets for Generalised Soundness Verification VMCAI Hadrien Bride Femto-ST / Université de Franche-Comté, Olga Kouchnarenko Femto-ST / Université de Franche-Comté, Fabien Peureux Femto-ST / Université de Franche-Comté + Smartesting S&S Media Attached | ||
15:00 30mTalk | Dynamic Reductions for Model Checking Concurrent Software. VMCAI Henning Günther Technische Universität Wien, Alfons Laarman Vienna University of Technology, Ana Sokolova University of Salzburg, Georg Weissenbacher Technische Universität Wien File Attached |