Bor-Yuh Evan Chang. Curriculum Vitæ EDUCATION ACADEMIC APPOINTMENTS RESEARCH INTERESTS AWARDS AND HONORS - PDF

Description
Bor-Yuh Evan Chang Curriculum Vitæ bec/ +1 (303) (phone) +1 (303) (fax) Department of Computer Science University of Colorado Boulder 430

Please download to get full document.

View again

of 15
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Information
Category:

Business & Economics

Publish on:

Views: 19 | Pages: 15

Extension: PDF | Download: 0

Share
Transcript
Bor-Yuh Evan Chang Curriculum Vitæ bec/ +1 (303) (phone) +1 (303) (fax) Department of Computer Science University of Colorado Boulder 430 UCB Boulder, CO USA EDUCATION PhD University of California, Berkeley, Computer Science 2008 Advisor: Prof. George C. Necula Thesis: End-User Program Analysis Dissertation Committee: Prof. George C. Necula (chair), Prof. Koushik Sen, and Prof. Jack Silver Proposal Committee: Prof. Rastislav Bodik (chair), Prof. Eric Brewer, Prof. George C. Necula, and Prof. Jack Silver MS University of California, Berkeley, Computer Science 2005 Advisor: Prof. George C. Necula Thesis: Type-Based Verification of Assembly Language Committee: Prof. George C. Necula and Prof. Rastislav Bodik BS Carnegie Mellon University, Computer Science, 4.0 GPA 2002 University and College Honors Minors: Biological Science and Mathematical Science Thesis: Iktara in ConCert: Realizing a Certified Grid Computing Framework from a Programmer s Perspective Advisors: Prof. Robert Harper and Prof. Frank Pfenning ACADEMIC APPOINTMENTS University of Colorado Boulder Assistant Professor, Department of Computer Science January 2009 present University of Maryland, College Park September 2008 November 2008 Postdoctoral Researcher, Department of Computer Science Advisor: Prof. Jeffrey S. Foster RESEARCH INTERESTS Algorithms, tools, and techniques for building, understanding, and ensuring reliable computational systems. Keywords: software quality, programmer productivity, program analysis, automated reasoning, programming languages, semantics, logic, formal methods. AWARDS AND HONORS Professional National Science Foundation CAREER Award December 2010 Graduate College of Engineering Graduate Student Prize December 2008 University of California, Berkeley Siebel Scholar, offered but declined because of graduation August 2008 University of California, Berkeley National Science Foundation Graduate Research Fellowship California Microelectronics Fellowship Undergraduate Phi Kappa Phi Honor Society, inducted May 2002 Andrew Carnegie Society Presidential Scholar, selected December 2001 Phi Beta Kappa Honor Society, inducted October 2001 Lambda Sigma Honor Society, inducted September 1999 Carnegie Mellon University Presidential and Institutional Scholarships Award Papers ECOOP 2013: Distinguished Artifact Award July 2013 QUIC Graphs: Relational Invariant Generation for Containers TACAS 2012: Journal Special Issue Invitation October 2012 A Bit Too Precise? Bounded Verification of Quantized Digital Filters GRANTS Awarded DARPA, MUSE: Mining and Understanding Bug Fixes to Address Application-Framework Protocol Defects, $1,599,343, 09/15/ /14/2018, Bor-Yuh Evan Chang (PI); Kenneth M. Anderson, Pavol Cerny, Sriram Sankaranarayanan, and Tom Yeh (co-pis). DARPA, APAC: Specialized Binary Analysis for Vetting Android Apps Using GUI Logic, $202,774 for CU, 09/01/ /31/2015 subcontract from University of Maryland, College Park, PI: Atif Memon, co-pis at CU: Tom Yeh and Bor-Yuh Evan Chang. NSF CCF , SHF: Small: Modular Reflection, $250,000, 10/01/ /30/2015, Bor-Yuh Evan Chang (PI); Jeremy G. Siek (co-pi). NSF CCF , CAREER: Cooperative Program Analysis: Bridging the Gap Between User and Tool Reasoning, $459,584, 06/01/ /31/2016, Bor-Yuh Evan Chang (PI). Joint Institute for Strategic Energy Analysis (JISEA) UGA , Verifiable Decision-Making Algorithms for Reconfiguration of Electric Microgrids, $49,985 total, $14,500 CU portion, 07/01/ /30/2011, Siddharth Suryanarayanan, Colorado State University and Sriram Sankaranarayanan (PIs); Bor-Yuh Evan Chang and Dirk Grunwald (co-pis). JISEA is affiliated with the National Renewable Energy Laboratory (NREL). NSF CCF , EAGER: Exploratory Research on Gradual Programming, $81,748, 08/01/ /31/2010, Jeremy G. Siek (PI); Bor-Yuh Evan Chang and Amer Diwan (co-pis). Bor-Yuh Evan Chang: Curriculum Vitæ (February 1, 2015) 2 ADVISING PhD Dissertation Advisees Alex Gendreau, in progress. Computer Science. University of Colorado Shawn Meier, in progress. Computer Science. University of Colorado Sam Blackshear, in progress. Computer Science. University of Colorado Devin Coughlin, defended January 7, Type-Intertwined Separation Logic. Computer Science. University of Colorado Arlen Cox, co-advised with Xavier Rival (ENS Paris) and Sriram Sankaranarayanan, defended November 17, Parametric Heap Abstraction for Dynamic Language Libraries. Electrical, Computer, and Energy Engineering. University of Colorado Research Advisees I have advised or co-advised independent studies or research projects for the following students. Aleksandar Chakarov (PhD), advised by Sriram Sankaranarayanan. Computer Science. University of Colorado Christoph Reichenbach (PhD 2009), advised by Amer Diwan. Computer Science. University of Colorado Robert Frohardt (PhD). Computer Science. University of Colorado Yi-Fan Tsai (MS). Computer Science. University of Colorado Daniel Stutzman (MS). Computer Science. University of Colorado Ross Holland (BS), Senior Thesis. Computer Science. University of Colorado Max Russek (BS). Computer Science. University of Colorado Evan Roncevich (BS), Discovery Learning Apprentice. Computer Science. University of Colorado Kyle Howell (BS), Discovery Learning Apprentice. Computer Science. University of Colorado Parker Evans (BS), co-advised with Pavol Cerny. Discovery Learning Apprentice. Computer Science. University of Colorado Nick Vanderweit (BS 2014), Senior Thesis. Computer Science. University of Colorado Alexander Beal (BS 2013), Senior Thesis. Computer Science. University of Colorado Kira Quan (BS). Computer Science. University of Colorado Chris Bubernak (BS), Discovery Learning Apprentice. Computer Science. University of Colorado James Holley (BS), Discovery Learning Apprentice. Electrical, Computer, and Energy Engineering. University of Colorado Bor-Yuh Evan Chang: Curriculum Vitæ (February 1, 2015) 3 CURRENT RESEARCH PROJECTS Nick Vanderweit (BS 2014), Senior Thesis. Computer Science. University of Colorado Alexander Beal (BS 2013), Senior Thesis. Computer Science. University of Colorado Kira Quan (BS). Computer Science. University of Colorado Chris Bubernak (BS), Discovery Learning Apprentice. Computer Science. University of Colorado James Holley (BS), Discovery Learning Apprentice. Electrical, Computer, and Energy Engineering. University of Colorado CURRENT RESEARCH PROJECTS University of Colorado Boulder 2012 Fissile Type Analysis: Modular Checking of Almost Everywhere Invariants Reflection is a language feature that reduces boilerplate and affords flexible and powerful frameworks. In current languages, however, the safety of reflection is checked only at run-time. In this project, we examine a modular, dependent type analysis that ensures compile-time reflection safety by checking refinement predicates relating mutable storage locations. With Devin Coughlin. University of Colorado Boulder 2012 Jsana: Abstract Domain Combinators for Dynamic Languages A hallmark of dynamic languages is the presence of libraries that emulate other language features using underlying dynamic features (e.g., class systems using JavaScript s open objects). In this project, we investigate abstract domain combinators to enable modular reasoning of the dynamic language features, such as open, dynamically-extendable objects, indirect property lookup, and property iteration. With Arlen Cox and Xavier Rival. University of Colorado Boulder 2012 Incremental Verification-Validation of Data Structure Invariants Reasoning about rich data structure invariants is notoriously difficult, making it a compelling but also challenging target for both static verification and dynamic validation. In this project, we examine leveraging static verification to synthesize dynamic validation code that soundly skips run-time checking whenever possible. With Yi-Fan Tsai, Devin Coughlin, and Xavier Rival. University of Colorado Boulder 2011 Thresher: Precise Heap Reachability by Refutation Analysis A resource leak occurs when a resource will no longer be used but fails to be recycled. Resource leaks are particularly pernicious bugs to detect and fix for the following reasons: (1) Their manifestation is often dependent on the execution environment (e.g., how much memory the device has); (2) Creating systematic tests for them is challenging (e.g., we need to assert there are no paths through the heap to a dead object); and (3) Off-the-shelf static analyses are typically too imprecise to be useful (i.e., have too many false alarms leaving a low signalto-noise ratio). Motivated by detecting Activity leak bugs in Android, we propose an approach that augments off-the-shelf points-to analyses with witness generation that aims to improve both the precision and the explainability of resource leak alarms. With Sam Blackshear and Manu Sridharan. University of Colorado Boulder 2010 Evidence-Generating Program Analysis In general, today s program analyzers provide poor explanations for their results. This issue limits their utility to everyday programmers. Such poor explanations are particularly problematic when analyzers report potential errors, as the user must decide whether the report is a real error or a false alarm due to an analyzer limitation. In this project, we devise algorithms for producing evidence for program analysis results. Importantly, this form of evidence will enable the analyzer user to interactively refine the results to identify real from false alarms. With Sam Blackshear, Sriram Sankaranarayanan, and Manu Sridharan. Bor-Yuh Evan Chang: Curriculum Vitæ (February 1, 2015) 4 SELECTED PAST RESEARCH PROJECTS University of Colorado Boulder Measuring Enforcements for Data-Driven Static Analysis Design Static analysis design is incredibly expensive, as many long iterations are required to determine whether or not a design is sufficient. We say that a static analysis design is sufficient if it can prove the property of interest with an acceptable number of false alarms. Ultimately, the only way to confirm that an analysis design is sufficient is to implement it and run it on real-world programs. If the evaluation shows that the design is insufficient, the designer must return to the drawing board and repeat the process. In this project, we observe that developers embed information in the form of enforcements that are both important to static analysis design and measurable with dynamic instrumentation. With Devin Coughlin, Jeremy G. Siek, and Amer Diwan. University of Colorado Boulder Verifying Reconfigurable Power Systems In this project, we look at how to find optimal placement of distributed generation and storage elements to enable reconfigurable smart-grid power systems. With Siddharth Suryanarayanan, Sriram Sankaranarayanan, and Dirk Grunwald. University of Colorado Boulder Gradual Programming There is no perfect programming language. Programmers must write code conforming to the idiosyncrasies of a programming language. Thus, there is often a disconnect between the intent of the developer and the meaning of the program. This semantic gap has a negative effect on programmer productivity, software reliability, and execution efficiency. In this project, we look to address this semantic gap through a drastic rethinking of how we develop software. With Devin Coughlin, Jeremy G. Siek, and Amer Diwan. University of Maryland, College Park Mix: Mixing Program Analyses Program analysis design is an exercise in tradeoffs. A precise analysis verifies deeper properties but may become prohibitively expensive to use, while a coarse analysis is efficient but suffers from high false alarm rates. In this project, we examine how to mix radically different analysis algorithms of varying precision that enables the analysis user (rather than the analysis designer) to make such tradeoffs. As a case study, we investigate the mixing of type inference (efficient) and symbolic evaluation (precise). With Khoo Yit Phang and Jeffrey S. Foster. University of California, Berkeley Xisa: Extensible Inductive Shape Analysis Shape analyses are unique in that they can capture detailed aliasing and structural information that is typically beyond the ability of other static program analyses. To do so, they rely on specialized data structure descriptions to build and decompose summaries of memory regions. Unfortunately, existing approaches suffer from usability and scalability issues that make them impractical to apply broadly. Typically, they either are insufficiently extensible or require low-level, expert interaction. Instead, our project focuses first on practicality by designing an extensible shape analysis based around high-level, program developer-oriented specifications. In particular, we observe that data structure checking code (e.g., used in testing or dynamic analysis) provides shape information that can also be used effectively in static analysis. With Xavier Rival and George Necula. REFEREED PUBLICATIONS IN PROCEEDINGS In many areas of Computer Science, including Programming Languages, the first and primary publication venues are full length papers in the proceedings of selective conferences. The two main outlets are proceedings published by ACM (Association for Computing Machinery) and the Lecture Notes in Computer Science (LNCS) series published by Springer. The DBLP service (http://dblp.uni-trier.de/db/) maintains an up-to-date index of Computer Science literature. In the following, the mark indicate students that I formally advise, and the mark indicate other student co-authors. Bor-Yuh Evan Chang: Curriculum Vitæ (February 1, 2015) 5 Arlen Cox, Bor-Yuh Evan Chang, and Xavier Rival Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages. In European Symposium on Programming (ESOP) of Lect Notes Comput Sc (April 2015). Acceptance: 28.7%. Arlen Cox, Bor-Yuh Evan Chang, and Xavier Rival Automatic Analysis of Open Objects in Dynamic Language Programs. In International Static Analysis Symposium (SAS), volume 8723 of Lect Notes Comput Sc (September 2014), Acceptance: 37.7%. Antoine Toubhans, Bor-Yuh Evan Chang, and Xavier Rival An Abstract Domain Combinator for Separately Conjoining Memory Abstractions. In International Static Analysis Symposium (SAS), volume 8723 of Lect Notes Comput Sc (September 2014), Acceptance: 37.7%. Arlen Cox, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers. In International Conference on Computer Aided Verification (CAV), volume 8859 of Lect Notes Comput Sc (July 2014), Acceptance: 24.9%. Devin Coughlin and Bor-Yuh Evan Chang Fissile Type Analysis: Modular Checking of Almost Everywhere Invariants. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), volume 49(1) of ACM SIGPLAN Notices (January 2014), Acceptance: 23.2%. Arlen Cox, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan QUIC Graphs: Relational Invariant Generation for Containers. In European Conference on Object-Oriented Programming (ECOOP), volume 7920 of Lect Notes Comput Sc (July 2013), Acceptance: 25.0%. Distinguished Artifact Award. Sam Blackshear, Bor-Yuh Evan Chang, and Manu Sridharan Thresher: Precise Refutations for Heap Reachability. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), volume 48(6) of ACM SIGPLAN Notices (June 2013), Acceptance: 17.2%. Antoine Toubhans, Bor-Yuh Evan Chang, and Xavier Rival Reduced Product Combination of Abstract Domains for Shapes. In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 7737 of Lect Notes Comput Sc (January 2013), Acceptance: 37.5%. Alejandro Sánchez, Sriram Sankaranarayanan, César Sánchez, and Bor-Yuh Evan Chang Invariant Generation for Parametrized Systems using Self-Reflection. In International Static Analysis Symposium (SAS), volume 7460 of Lect Notes Comput Sc (September 2012), Acceptance: 40.3%. Devin Coughlin, Bor-Yuh Evan Chang, Amer Diwan, and Jeremy G. Siek Measuring Enforcement Windows with Symbolic Trace Interpretation: What Well-Behaved Programs Say. In International Symposium on Software Testing and Analysis (ISSTA) (July 2012), Acceptance: 28.7%. Arlen Cox, Sriram Sankaranarayanan, and Bor-Yuh Evan Chang A Bit Too Precise? Bounded Verification of Quantized Digital Filters. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 7214 of Lect Notes Comput Sc (March 2012), Acceptance: 24.5%. Sam Blackshear, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Manu Sridharan The Flow- Insensitive Precision of Andersen s Analysis in Practice. In International Static Analysis Symposium (SAS), volume 6887 of Lect Notes Comput Sc (September 2011), Acceptance: 32.8%. Xavier Rival and Bor-Yuh Evan Chang Calling Context Abstraction with Shapes. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), volume 46(1) of ACM SIGPLAN Notices (January 2011), Acceptance: 23.4%. Robert Frohardt, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan Access Nets: Modeling Access to Physical Spaces. In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) of Lect Notes Comput Sc (January 2011), Acceptance: 33.8%. Khoo Yit Phang, Bor-Yuh Evan Chang, and Jeffrey S. Foster Mixing Type Checking and Symbolic Execution. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), volume 45(6) of ACM SIGPLAN Notices (June 2010), Acceptance: 20.1%. Bor-Yuh Evan Chang: Curriculum Vitæ (February 1, 2015) 6 Vincent Laviron, Bor-Yuh Evan Chang, and Xavier Rival Separating Shape Graphs. In European Symposium on Programming (ESOP), volume 6012 of Lect Notes Comput Sc (March 2010), Acceptance: 24.8%. Bor-Yuh Evan Chang and Xavier Rival Relational Inductive Shape Analysis. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), volume 43(1) of ACM SIGPLAN Notices (January 2008), Acceptance: 16.5%. Bor-Yuh Evan Chang, Xavier Rival, and George C. Necula Shape Analysis with Structural Invariant Checkers. In International Static Analysis Symposium (SAS), volume 4634 of Lect Notes Comput Sc (August 2007), Acceptance: 30.6%. Bor-Yuh Evan Chang, Matthew Harren, and George C. Necula Analysis of Low-Level Code Using Cooperating Decompilers. In International Static Analysis Symposium (SAS), volume 4134 of Lect Notes Comput Sc (August 2006), Acceptance: 28.8%. Bor-Yuh Evan Chang, Adam Chlipala, and George C. Necula A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) of Lect Notes Comput Sc (January 2006), Acceptance: 48.3%. Bor-Yuh Evan Chang and K. Rustan M. Leino Abstract Interpretation with Alien Expressions and Heap Structures. In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) of Lect Notes Comput Sc (January 2005), Acceptance: 29.3%. REFEREED JOURNAL PUBLICATIONS Arlen Cox, Sriram Sankaranarayanan, and Bor-Yuh Evan Chang A Bit Too Precise? Verification of Quantized Digital Filters. Int J Softw Tools Technol Transfer (2014), volume 16(2), PEER-REVIEWED INVITED PUBLICATIONS Xavier Rival, Antoine Toubhans, and Bor-Yuh Evan Chang Construction of Abstract Domains for Heterogeneous Properties (Position Paper). In International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA), volume 8803 of Lect Notes Comput Sc (October 2014), Bor-Yuh Evan Chang and Xavier Rival Modular Construction of Shape-Numeric Analyzers. In Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday (SAIRP), volume 129 of Electr P in Theor Comput Sc (September 2013). Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino
Related Search
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks