Trustless Grid Computing in ConCert. - Bor-Yuh Evan Chang; Karl Crary; Margaret DeLap; Robert Harper 001; Jason Liszka; Tom Murphy VII; Frank Pfenning (GRID, 2002)

PML: Toward a High-Level Formal Language for Biological Systems. - Bor-Yuh Evan Chang; Manu Sridharan (BioConcur@CONCUR, 2003)

Boogie: A Modular Reusable Verifier for Object-Oriented Programs. - Michael Barnett 001; Bor-Yuh Evan Chang; Robert DeLine; Bart Jacobs 002; K. Rustan M. Leino (FMCO, 2005)

The open verifier framework for foundational verifiers. - Bor-Yuh Evan Chang; Adam Chlipala; George C. Necula; Robert R. Schneck (TLDI, 2005)

Type-based verification of assembly language for compiler debugging. - Bor-Yuh Evan Chang; Adam Chlipala; George C. Necula; Robert R. Schneck (TLDI, 2005)

Abstract Interpretation with Alien Expressions and Heap Structures. - Bor-Yuh Evan Chang; K. Rustan M. Leino (VMCAI, 2005)

Inferring Object Invariants: Extended Abstract. - Bor-Yuh Evan Chang; K. Rustan M. Leino (AIOOL@VMCAI, 2005)

Analysis of Low-Level Code Using Cooperating Decompilers. - Bor-Yuh Evan Chang; Matthew Harren; George C. Necula (SAS, 2006)

A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. - Bor-Yuh Evan Chang; Adam Chlipala; George C. Necula (VMCAI, 2006)

Shape Analysis with Structural Invariant Checkers. - Bor-Yuh Evan Chang; Xavier Rival; George C. Necula (SAS, 2007)

Relational inductive shape analysis. - Bor-Yuh Evan Chang; Xavier Rival (POPL, 2008)

Separating Shape Graphs. - Vincent Laviron; Bor-Yuh Evan Chang; Xavier Rival (ESOP, 2010)

Mixing type checking and symbolic execution. - Yit Phang Khoo; Bor-Yuh Evan Chang; Jeffrey S. Foster (PLDI, 2010)

Calling context abstraction with shapes. - Xavier Rival; Bor-Yuh Evan Chang (POPL, 2011)

The Flow-Insensitive Precision of Andersen's Analysis in Practice. - Sam Blackshear; Bor-Yuh Evan Chang; Sriram Sankaranarayanan 001; Manu Sridharan (SAS, 2011)

Access Nets: Modeling Access to Physical Spaces. - Robert Frohardt; Bor-Yuh Evan Chang; Sriram Sankaranarayanan 001 (VMCAI, 2011)

Measuring enforcement windows with symbolic trace interpretation: what well-behaved programs say. - Devin Coughlin; Bor-Yuh Evan Chang; Amer Diwan; Jeremy G. Siek (ISSTA, 2012)

Invariant Generation for Parametrized Systems Using Self-reflection - (Extended Version). - Alejandro Sánchez; Sriram Sankaranarayanan 001; César Sánchez 001; Bor-Yuh Evan Chang (SAS, 2012)

A Bit Too Precise? Bounded Verification of Quantized Digital Filters. - Arlen Cox; Sriram Sankaranarayanan 001; Bor-Yuh Evan Chang (TACAS, 2012)

QUIC Graphs: Relational Invariant Generation for Containers. - Arlen Cox; Bor-Yuh Evan Chang; Sriram Sankaranarayanan 001 (ECOOP, 2013)

Thresher: precise refutations for heap reachability. - Sam Blackshear; Bor-Yuh Evan Chang; Manu Sridharan (PLDI, 2013)

Reduced Product Combination of Abstract Domains for Shapes. - Antoine Toubhans; Bor-Yuh Evan Chang; Xavier Rival (VMCAI, 2013)

Modular Construction of Shape-Numeric Analyzers. - Bor-Yuh Evan Chang; Xavier Rival (Festschrift for Dave Schmidt, 2013)

Preface. - Bor-Yuh Evan Chang (TAPAS@SAS, 2013)

QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers. - Arlen Cox; Bor-Yuh Evan Chang; Sriram Sankaranarayanan 001 (CAV, 2014)

Android apps consistency scrutinized. - Khalid Alharbi; Sam Blackshear; Emily Kowalczyk; Atif M. Memon; Bor-Yuh Evan Chang; Tom Yeh (CHI Extended Abstracts, 2014)

Construction of Abstract Domains for Heterogeneous Properties (Position Paper). - Xavier Rival; Antoine Toubhans; Bor-Yuh Evan Chang (ISoLA (2), 2014)

Fissile type analysis: modular checking of almost everywhere invariants. - Devin Coughlin; Bor-Yuh Evan Chang (POPL, 2014)

Automatic Analysis of Open Objects in Dynamic Language Programs. - Arlen Cox; Bor-Yuh Evan Chang; Xavier Rival (SAS, 2014)

An Abstract Domain Combinator for Separately Conjoining Memory Abstractions. - Antoine Toubhans; Bor-Yuh Evan Chang; Xavier Rival (SAS, 2014)

Refuting Heap Reachability. - Bor-Yuh Evan Chang (VMCAI, 2014)

A bit too precise? Verification of quantized digital filters. - Arlen Cox; Sriram Sankaranarayanan 001; Bor-Yuh Evan Chang (Int. J. Softw. Tools Technol. Transf., 2014)

Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages. - Arlen Cox; Bor-Yuh Evan Chang; Xavier Rival (ESOP, 2015)

Abstract Domains and Solvers for Sets Reasoning. - Arlen Cox; Bor-Yuh Evan Chang; Huisong Li; Xavier Rival (LPAR, 2015)

Selective control-flow abstraction via jumping. - Sam Blackshear; Bor-Yuh Evan Chang; Manu Sridharan (OOPSLA, 2015)

Droidel: a general approach to Android framework modeling. - Sam Blackshear; Alexandra Gendreau; Bor-Yuh Evan Chang (SOAP@PLDI, 2015)

Shape Analysis for Unstructured Sharing. - Huisong Li; Xavier Rival; Bor-Yuh Evan Chang (SAS, 2015)

In defense of soundiness: a manifesto. - Benjamin Livshits; Manu Sridharan; Yannis Smaragdakis; Ondrej Lhoták; José Nelson Amaral; Bor-Yuh Evan Chang; Samuel Z. Guyer; Uday P. Khedker; Anders Møller; Dimitrios Vardoulakis (Commun. ACM, 2015)

Synthesizing Short-Circuiting Validation of Data Structure Invariants. - Yi-Fan Tsai; Devin Coughlin; Bor-Yuh Evan Chang; Xavier Rival (CoRR, 2015)

A vision for online verification-validation. - Matthew A. Hammer; Bor-Yuh Evan Chang; David Van Horn (GPCE, 2016)

ChimpCheck: property-based randomized test generation for interactive apps. - Edmund S. L. Lam; Peilun Zhang; Bor-Yuh Evan Chang (Onward!, 2017)

Semantic-directed clumping of disjunctive abstract states. - Huisong Li; Francois Berenger; Bor-Yuh Evan Chang; Xavier Rival (POPL, 2017)

Discriminating Traces with Time. - Saeid Tizpaz-Niari; Pavol Cerný; Bor-Yuh Evan Chang; Sriram Sankaranarayanan 001; Ashutosh Trivedi 001 (TACAS (2), 2017)

Abstracting Event-Driven Systems with Lifestate Rules. - Shawn Meier; Aleksandar Chakarov; Maxwell Russek; Sergio Mover; Bor-Yuh Evan Chang (CoRR, 2017)

Learning Asynchronous Typestates for Android Classes. - Arjun Radhakrishna; Nicholas V. Lewchenko; Shawn Meier; Sergio Mover; Krishna Chaitanya Sripada; Damien Zufferey; Bor-Yuh Evan Chang; Pavol Cerný (CoRR, 2017)

Memory Abstraction, Emerging Techniques and Applications (NII Shonan Meeting 2017-12). - Bor-Yuh Evan Chang; Xavier Rival; Sukyoung Ryu (NII Shonan Meet. Rep., 2017)

Differential Performance Debugging With Discriminant Regression Trees. - Saeid Tizpaz-Niari; Pavol Cerný; Bor-Yuh Evan Chang; Ashutosh Trivedi 001 (AAAI, 2018)

DroidStar: callback typestates for Android classes. - Arjun Radhakrishna; Nicholas V. Lewchenko; Shawn Meier; Sergio Mover; Krishna Chaitanya Sripada; Damien Zufferey; Bor-Yuh Evan Chang; Pavol Cerný (ICSE, 2018)

Safe stream-based programming with refinement types. - Benno Stein 002; Lazaro Clapp; Manu Sridharan; Bor-Yuh Evan Chang (ASE, 2018)

Mining framework usage graphs from app corpora. - Sergio Mover; Sriram Sankaranarayanan 001; Rhys Braginton Pettee Olsen; Bor-Yuh Evan Chang (SANER, 2018)

Lifestate: Event-Driven Protocols and Callback Control Flow. - Shawn Meier; Sergio Mover; Bor-Yuh Evan Chang (ECOOP, 2019)

Type-Directed Bounding of Collections in Reactive Programs. - Tianhan Lu; Pavol Cerný; Bor-Yuh Evan Chang; Ashutosh Trivedi 001 (VMCAI, 2019)

Lifestate: Event-Driven Protocols and Callback Control Flow (Extended Version). - Shawn Meier; Sergio Mover; Bor-Yuh Evan Chang (CoRR, 2019)

Lifestate: Event-Driven Protocols and Callback Control Flow (Artifact). - Shawn Meier; Sergio Mover; Bor-Yuh Evan Chang (Dagstuhl Artifacts Ser., 2019)

Static analysis with demand-driven value refinement. - Benno Stein 002; Benjamin Barslev Nielsen; Bor-Yuh Evan Chang; Anders Møller (Proc. ACM Program. Lang., 2019)

Shape Analysis. - Bor-Yuh Evan Chang; Cezara Dragoi; Roman Manevich; Noam Rinetzky; Xavier Rival (Found. Trends Program. Lang., 2020)

Demanded abstract interpretation. - Benno Stein 002; Bor-Yuh Evan Chang; Manu Sridharan (PLDI, 2021)

Selectively-Amortized Resource Bounding. - Tianhan Lu; Bor-Yuh Evan Chang; Ashutosh Trivedi 001 (SAS, 2021)

Demanded Abstract Interpretation (Extended Version). - Benno Stein 002; Bor-Yuh Evan Chang; Manu Sridharan (CoRR, 2021)

Differential cost analysis with simultaneous potentials and anti-potentials. - Dorde Zikelic; Bor-Yuh Evan Chang; Pauline Bolignano; Franco Raimondi (PLDI, 2022)

Lifting On-Demand Analysis to Higher-Order Languages. - Daniel Schoepe; David Seekatz; Ilina Stoilkovska; Sandro Stucki; Daniel Tattersall; Pauline Bolignano; Franco Raimondi; Bor-Yuh Evan Chang (SAS, 2023)

Historia: Refuting Callback Reachability with Message-History Logics (Extended Version). - Shawn Meier; Sergio Mover; Gowtham Kaki; Bor-Yuh Evan Chang (CoRR, 2023)

Historia: Refuting Callback Reachability with Message-History Logics. - Shawn Meier; Sergio Mover; Gowtham Kaki; Bor-Yuh Evan Chang (Proc. ACM Program. Lang., 2023)

Interactive Abstract Interpretation with Demanded Summarization. - Benno Stein 001; Bor-Yuh Evan Chang; Manu Sridharan (ACM Trans. Program. Lang. Syst., 2024)

Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering. - Jiawei Yang; Xiao Cheng 002; Bor-Yuh Evan Chang; Xiapu Luo; Yulei Sui (ECOOP, 2025)

Bolt-On Strong Consistency: Specification, Implementation, and Verification. - Nicholas V. Lewchenko; Gowtham Kaki; Bor-Yuh Evan Chang (Proc. ACM Program. Lang., 2025)

JoelYYoung/RecTopo. - Jiawei Yang; Xiao Cheng 002; Bor-Yuh Evan Chang; Xiapu Luo; Yulei Sui (DROPS Artifacts, 2025)