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 | Formulog: Datalog for SMT-Based Static Analysis OOPSLA Link to publication DOI Media Attached | ||
09:20 - 09:40 Talk | A Large-Scale Longitudinal Study of Flaky Tests 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 | Handling Bidirectional Control Flow 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 | WATCHER: In-Situ Failure Diagnosis 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 | Formulog: Datalog for SMT-Based Static Analysis OOPSLA Link to publication DOI Media Attached | ||
21:20 - 21:40 Talk | A Large-Scale Longitudinal Study of Flaky Tests 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 | Handling Bidirectional Control Flow 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 | WATCHER: In-Situ Failure Diagnosis 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 |