SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 09:00 - 09:20 at SPLASH-I - T-2 Chair(s): Karim Ali, Aritra Sengupta
Tue 17 Nov 2020 21:00 - 21:20 at SPLASH-I - T-2 Chair(s): Yaoda Zhou, Iulian Neamtiu

Satisfiability modulo theories (SMT) solving has become a critical part of many static analyses, including symbolic execution, refinement type checking, and model checking. We propose Formulog, a domain-specific language that makes it possible to write a range of SMT-based static analyses in a way that is both close to their formal specifications and amenable to high-level optimizations and efficient evaluation.

Formulog extends the logic programming language Datalog with a first-order functional language and mechanisms for representing and reasoning about SMT formulas; a novel type system supports the construction of expressive formulas, while ensuring that neither normal evaluation nor SMT solving goes wrong. Our case studies demonstrate that a range of SMT-based analyses can naturally and concisely be encoded in Formulog, and that — thanks to this encoding — high-level Datalog-style optimizations can be automatically and advantageously applied to these analyses.

Tue 17 Nov

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

09:00 - 10:20
T-2OOPSLA at SPLASH-I +12h
Chair(s): Karim Ali University of Alberta, Aritra Sengupta Amazon Web Services, USA
09:00
20m
Talk
Formulog: Datalog for SMT-Based Static Analysis
OOPSLA
Aaron Bembenek Harvard University, Michael Greenberg Pomona College, Stephen Chong Harvard University
Link to publication DOI Media Attached
09:20
20m
Talk
A Large-Scale Longitudinal Study of Flaky Tests
OOPSLA
Wing Lam University of Illinois at Urbana-Champaign, Stefan Winter TU Darmstadt, Anjiang Wei Peking University, Tao Xie Peking University, Darko Marinov University of Illinois at Urbana-Champaign, Jonathan Bell Northeastern University
Link to publication DOI Media Attached
09:40
20m
Talk
Handling Bidirectional Control Flow
OOPSLA
Yizhou Zhang University of Waterloo, Guido Salvaneschi University of St. Gallen, Andrew Myers Cornell University
Link to publication DOI Media Attached
10:00
20m
Talk
WATCHER: In-Situ Failure Diagnosis
OOPSLA
Hongyu Liu Purdue University, Sam Silvestro University of Texas at San Antonio, Xiangyu Zhang Purdue University, Jian Huang University of Illinois at Urbana-Champaign, Tongping Liu University of Massachusetts at Amherst
Link to publication DOI Media Attached
21:00 - 22:20
T-2OOPSLA at SPLASH-I
Chair(s): Yaoda Zhou University of Hong Kong, Iulian Neamtiu New Jersey Institute of Technology
21:00
20m
Talk
Formulog: Datalog for SMT-Based Static Analysis
OOPSLA
Aaron Bembenek Harvard University, Michael Greenberg Pomona College, Stephen Chong Harvard University
Link to publication DOI Media Attached
21:20
20m
Talk
A Large-Scale Longitudinal Study of Flaky Tests
OOPSLA
Wing Lam University of Illinois at Urbana-Champaign, Stefan Winter TU Darmstadt, Anjiang Wei Peking University, Tao Xie Peking University, Darko Marinov University of Illinois at Urbana-Champaign, Jonathan Bell Northeastern University
Link to publication DOI Media Attached
21:40
20m
Talk
Handling Bidirectional Control Flow
OOPSLA
Yizhou Zhang University of Waterloo, Guido Salvaneschi University of St. Gallen, Andrew Myers Cornell University
Link to publication DOI Media Attached
22:00
20m
Talk
WATCHER: In-Situ Failure Diagnosis
OOPSLA
Hongyu Liu Purdue University, Sam Silvestro University of Texas at San Antonio, Xiangyu Zhang Purdue University, Jian Huang University of Illinois at Urbana-Champaign, Tongping Liu University of Massachusetts at Amherst
Link to publication DOI Media Attached