Write a Blog >>
Wed 21 Jun 2017 15:55 - 16:20 at Auditorium, Vertex Building - Analysis and Synthesis Chair(s): Anders Møller

Stateless Model Checking (SMC) offers a powerful approach to verifying multithreaded programs but suffers from the state-space explosion problem caused by the huge thread interleaving space. The pioneering reduction technique Partial Order Reduction (POR) mitigates this problem by pruning equivalent interleavings from the state space. However, limited by the happens-before relation, POR still explores redundant executions. The recent advance, Maximal Causality Reduction (MCR), shows a promising performance improvement over the existing reduction techniques. However, MCR is limited to the dynamic information of the program and has to construct com- plicated constraints to ensure the feasibility of the derived execution. Unfortunately, the intricate constraints can greatly slow down the exploration of the state space. In this work, we present a new technique, which extends MCR with static analysis to reduce the size of the constraints, thus speeding up the efficiency of the state space exploration. We use system dependency graph to capture the dependency between a read and a later event e in the trace and identify those reads that e is not control dependent on. We then ignore the constraints over such reads and hence reduce the size of the constraints. The experimental results show that compared to MCR, the number of the constraints and the solving time by our approach are averagely reduced by 31.6% and 27.8%, respectively.

Wed 21 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:30 - 17:10
Analysis and SynthesisECOOP Research Papers at Auditorium, Vertex Building
Chair(s): Anders Møller Aarhus University
15:30
25m
Talk
Proactive Synthesis of Recursive Tree-to-String Functions from Examples
ECOOP Research Papers
Mikaël Mayer EPFL, Switzerland, Jad Hamza LIAFA, Université Paris Diderot, Viktor Kunčak EPFL, Switzerland
Link to publication Media Attached
15:55
25m
Talk
Speeding Up Maximal Causality Reduction with Static Dependency Analysis
ECOOP Research Papers
Shiyou Huang Texas A&M University, Jeff Huang Texas A&M University
Link to publication Media Attached
16:20
25m
Talk
Mailbox Abstractions for Static Analysis of Actor Programs
ECOOP Research Papers
Quentin Stiévenart Vrije Universiteit Brussel, Belgium, Jens Nicolay Vrije Universiteit Brussel, Belgium, Wolfgang De Meuter Vrije Universiteit Brussel, Coen De Roover Vrije Universiteit Brussel
Link to publication Pre-print Media Attached
16:45
25m
Talk
What’s the Optimal Performance of Precise Dynamic Race Detection? – A Redundancy Perspective
ECOOP Research Papers
Jeff Huang Texas A&M University, Arun Krishnakumar Rajagopalan Texas A&M University
Link to publication Media Attached