SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 09:00 - 09:20 at OOPSLA/ECOOP - T-2
Tue 17 Nov 2020 21:00 - 21:20 at OOPSLA/ECOOP - T-2

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 OOPSLA/ECOOP +12h
09:00 - 09:20
Talk
OOPSLA
Aaron BembenekHarvard University, Michael GreenbergPomona College, Stephen ChongHarvard University
09:20 - 09:40
Talk
OOPSLA
Wing LamUniversity of Illinois at Urbana-Champaign, Stefan WinterTU Darmstadt, Germany, Anjiang WeiPeking University, Tao XiePeking University, Darko MarinovUniversity of Illinois at Urbana-Champaign, Jonathan BellNortheastern University
09:40 - 10:00
Talk
OOPSLA
Yizhou ZhangUniversity of Waterloo, Guido SalvaneschiUniversity of St. Gallen, Andrew MyersCornell University
10:00 - 10:20
Talk
OOPSLA
Hongyu LiuPurdue University, Sam SilvestroUniversity of Texas at San Antonio, USA, Xiangyu ZhangPurdue University, USA, Jian HuangUniversity of Illinois at Urbana-Champaign, Tongping LiuUniversity of Massachusetts Amherst
21:00 - 22:20: T-2OOPSLA at OOPSLA/ECOOP
21:00 - 21:20
Talk
OOPSLA
Aaron BembenekHarvard University, Michael GreenbergPomona College, Stephen ChongHarvard University
21:20 - 21:40
Talk
OOPSLA
Wing LamUniversity of Illinois at Urbana-Champaign, Stefan WinterTU Darmstadt, Germany, Anjiang WeiPeking University, Tao XiePeking University, Darko MarinovUniversity of Illinois at Urbana-Champaign, Jonathan BellNortheastern University
21:40 - 22:00
Talk
OOPSLA
Yizhou ZhangUniversity of Waterloo, Guido SalvaneschiUniversity of St. Gallen, Andrew MyersCornell University
22:00 - 22:20
Talk
OOPSLA
Hongyu LiuPurdue University, Sam SilvestroUniversity of Texas at San Antonio, USA, Xiangyu ZhangPurdue University, USA, Jian HuangUniversity of Illinois at Urbana-Champaign, Tongping LiuUniversity of Massachusetts Amherst