ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Mon 8 Apr 2019 17:00 - 17:30 at SUN I - SAT Solving and Theorem Proving Chair(s): Armin Biere

The Alloy tool-set has been widely used in software design and analysis. However, Alloy Analyzer that automates a bounded exhaustive analysis relies on expensive SAT solving. Recent studies have shown that users often perform consecutive analysis with slightly different models, which opens up the possibility of using incremental analysis for speeding up the interaction. In this paper, we aim to develop an incremental analysis to reduce the number SAT invocations, thus speeding up the evolving Alloy analysis. Firstly, we proposed Regression Command Selection based on dependency analysis, similar to those used by Regression Test Selection, to select the commands only affected by users’ changes. Secondly, we applied Solution Reuse on the selected commands to further reduce the actual command execution (which invokes SAT solving). Our experimental results show that our approach significantly outperforms Alloy Analyzer in the analysis of evolving Alloy models.

Mon 8 Apr

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

16:30 - 18:00
SAT Solving and Theorem ProvingTACAS at SUN I
Chair(s): Armin Biere Johannes Kepler University Linz
16:30
30m
Talk
Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks
TACAS
Pengfei Gao , Hongyi Xie , Jun Zhang , Fu Song , Taolue Chen Birkbeck, University of London
Link to publication
17:00
30m
Talk
Incremental Analysis of Evolving Alloy Models
TACAS
Wenxi Wang The University of Texas at Austin, Texas, USA, Kaiyuan Wang Google, Inc., Milos Gligoric University of Texas at Austin, Sarfraz Khurshid University of Texas at Austin
Link to publication
17:30
30m
Talk
Extending a Brainiac Prover to Lambda-Free Higher-Order Logic
TACAS
Link to publication