SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 07:40 - 08:00 at SPLASH-III - F-1B Chair(s): Aviral Goel, Sophia Drossopoulou
Fri 20 Nov 2020 19:40 - 20:00 at SPLASH-III - F-1B Chair(s): Alex Potanin, Steve Blackburn

Formally verifying software correctness is a highly manual process. However,
because verification proof scripts often share structure, it is possible to
learn from existing proof scripts to fully automate some formal verification.
The goal of this paper is to improve proof script synthesis and enable fully
automating more verification. Interactive theorem provers, such as the Coq
proof assistant, allow programmers to write partial proof scripts, observe
the semantics of the proof state thus far, and then attempt more progress.
Knowing the proof state semantics is a significant aid. Recent research has
shown that the proof state can help predict the next step. In this paper, we
present TacTok, the first technique that attempts to fully automate proof
script synthesis by modeling proof scripts using both the partial proof
script written thus far and the semantics of the proof state. Thus, TacTok
more completely models the information the programmer has access to when
writing proof scripts manually. We evaluate TacTok on a benchmark of 26
software projects in Coq, consisting of over 10 thousand theorems. We compare
our approach to five tools. Two prior techniques, CoqHammer, the
state-of-the-art proof synthesis technique, and ASTactic, a proof script
synthesis technique that models proof state. And three new proof script
synthesis technique we create ourselves, SeqOnly, which models only the
partial proof script and the initial theorem being proven, and WeightedRandom
and WeightedGreedy, which use metaheuristic search biased by frequencies of
proof tactics in existing, successful proof scripts. We find that TacTok
outperforms WeightedRandom and WeightedGreedy, and is complementary to
CoqHammer and ASTactic: for 24 out of the 26 projects, TacTok can synthesize
proof scripts for some theorems the prior tools cannot. Together with TacTok,
11.5% more theorems can be proven automatically than by CoqHammer alone, and
20.0% than by ASTactic alone. Compared to a combination of CoqHammer and
ASTactic, TacTok can prove an additional 3.6% more theorems, proving 115
theorems no tool could previously prove. Overall, our experiments provide
evidence that partial proof script and proof state semantics, together,
provide useful information for proof script modeling, and that metaheuristic
search is a promising direction for proof script synthesis. TacTok is
open-source and we make public all our data and a replication package of our
experiments.

Fri 20 Nov
Times are displayed in time zone: Central Time (US & Canada) change

07:00 - 08:20: F-1BOOPSLA at SPLASH-III +12h
Chair(s): Aviral GoelNortheastern University, Sophia DrossopoulouImperial College London
07:00 - 07:20
Talk
OOPSLA
Qianshan YuTsinghua University, Fei HeTsinghua University, Bow-Yaw WangAcademia Sinica
Link to publication DOI Media Attached
07:20 - 07:40
Talk
OOPSLA
Minseok JeonKorea University, Myungho LeeKorea University, Hakjoo OhKorea University
Link to publication DOI Media Attached
07:40 - 08:00
Talk
OOPSLA
Emily FirstUniversity of Massachusetts at Amherst, Yuriy BrunUniversity of Massachusetts Amherst, Arjun GuhaUniversity of Massachusetts at Amherst
Link to publication DOI Pre-print Media Attached
08:00 - 08:20
Talk
OOPSLA
Ruyi JiPeking University, Yican SunPeking University, Yingfei XiongPeking University, Zhenjiang HuPeking University
Link to publication DOI Media Attached
19:00 - 20:20: F-1BOOPSLA at SPLASH-III
Chair(s): Alex PotaninVictoria University of Wellington, Steve BlackburnAustralian National University
19:00 - 19:20
Talk
OOPSLA
Qianshan YuTsinghua University, Fei HeTsinghua University, Bow-Yaw WangAcademia Sinica
Link to publication DOI Media Attached
19:20 - 19:40
Talk
OOPSLA
Minseok JeonKorea University, Myungho LeeKorea University, Hakjoo OhKorea University
Link to publication DOI Media Attached
19:40 - 20:00
Talk
OOPSLA
Emily FirstUniversity of Massachusetts at Amherst, Yuriy BrunUniversity of Massachusetts Amherst, Arjun GuhaUniversity of Massachusetts at Amherst
Link to publication DOI Pre-print Media Attached
20:00 - 20:20
Talk
OOPSLA
Ruyi JiPeking University, Yican SunPeking University, Yingfei XiongPeking University, Zhenjiang HuPeking University
Link to publication DOI Media Attached