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): Iulian Neamtiu, Yaoda Zhou

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
Times are displayed in time zone: Central Time (US & Canada) change

09:00 - 10:20: T-2OOPSLA at SPLASH-I +12h
Chair(s): Karim AliUniversity of Alberta, Aritra SenguptaAmazon Web Services, USA
09:00 - 09:20
Talk
OOPSLA
Aaron BembenekHarvard University, Michael GreenbergPomona College, Stephen ChongHarvard University
Link to publication DOI Media Attached
09:20 - 09:40
Talk
OOPSLA
Wing LamUniversity of Illinois at Urbana-Champaign, Stefan WinterTU Darmstadt, Anjiang WeiPeking University, Tao XiePeking University, Darko MarinovUniversity of Illinois at Urbana-Champaign, Jonathan BellNortheastern University
Link to publication DOI Media Attached
09:40 - 10:00
Talk
OOPSLA
Yizhou ZhangUniversity of Waterloo, Guido SalvaneschiUniversity of St. Gallen, Andrew C. MyersCornell University
Link to publication DOI Media Attached
10:00 - 10:20
Talk
OOPSLA
Hongyu LiuPurdue University, Sam SilvestroUniversity of Texas at San Antonio, Xiangyu ZhangPurdue University, Jian HuangUniversity of Illinois at Urbana-Champaign, Tongping LiuUniversity of Massachusetts at Amherst
Link to publication DOI Media Attached
21:00 - 22:20: T-2OOPSLA at SPLASH-I
Chair(s): Iulian NeamtiuNew Jersey Institute of Technology, Yaoda ZhouUniversity of Hong Kong
21:00 - 21:20
Talk
OOPSLA
Aaron BembenekHarvard University, Michael GreenbergPomona College, Stephen ChongHarvard University
Link to publication DOI Media Attached
21:20 - 21:40
Talk
OOPSLA
Wing LamUniversity of Illinois at Urbana-Champaign, Stefan WinterTU Darmstadt, Anjiang WeiPeking University, Tao XiePeking University, Darko MarinovUniversity of Illinois at Urbana-Champaign, Jonathan BellNortheastern University
Link to publication DOI Media Attached
21:40 - 22:00
Talk
OOPSLA
Yizhou ZhangUniversity of Waterloo, Guido SalvaneschiUniversity of St. Gallen, Andrew C. MyersCornell University
Link to publication DOI Media Attached
22:00 - 22:20
Talk
OOPSLA
Hongyu LiuPurdue University, Sam SilvestroUniversity of Texas at San Antonio, Xiangyu ZhangPurdue University, Jian HuangUniversity of Illinois at Urbana-Champaign, Tongping LiuUniversity of Massachusetts at Amherst
Link to publication DOI Media Attached