Gordon, Colin S., Matskevich, Sergey
Onward! Papers, October 2023, doi: 10.1145/3622758.3622890
Interactive proof assistants are computer programs carefully constructed to check a human-designed proof of a mathematical claim with high confidence in the implementation. However, this only validates truth of a formal claim, which may have been mis…
pdf url acm youtube arXivGordon, Colin S., Yun, Chaewon
30th Annual Static Analysis Symposium (SAS), October 2023, doi: 10.1007/978-3-031-44245-2_16
We describe a new concrete approach to giving predictable error locations for sequential (flow-sensitive) effect systems. Prior implementations of sequential effect systems rely on either computing a bottom-up effect and comparing it to a declaration…
pdf url springer youtube arXivGordon, Colin S.
44th IEEE/ACM International Conference on Software Engineering: New Ideas and Emerging Results, ICSE (NIER), May 2022, doi: 10.1145/3510455.3512781
We consider a new approach to generate tests from natural language. Rather than relying on machine learning or templated extraction from structured comments, we propose to apply classic ideas from linguistics to translate natural-language sentences i…
pdf url youtube arXivGordon, Colin S.
ACM Transactions on Programming Languages and Systems (TOPLAS), volume 43, number 1, April 2021, doi: 10.1145/3450272
Effect systems are lightweight extensions to type systems that can verify a wide range of important properties with modest developer burden. But our general understanding of effect systems is limited primarily to systems where the order of effects is…
pdf url acm arXivGordon, Colin S.
Proceedings of the 34th European Conference on Object-Oriented Programming (ECOOP'20), July 2020, doi: 10.4230/LIPIcs.ECOOP.2020.10
Capabilities (whether object or reference capabilities) are fundamentally tools to restrict effects. Thus static capabilities (object or reference) and effect systems take different technical machinery to the same core problem of statically restricti…
pdf lipics youtube arXivGordon, Colin S.
Proceedings of the 34th European Conference on Object-Oriented Programming (ECOOP'20), July 2020, doi: 10.4230/LIPIcs.ECOOP.2020.23
Sequential effect systems are a class of effect system that exploits information about program order, rather than discarding it as traditional commutative effect systems do. This extra expressive power allows effect systems to reason about behavior …
pdf lipics youtube arXivGordon, Colin S.
ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control (AGERE 2019), October 2019, doi: 10.1145/3358499.3361221
The actor model is a well-established way to approach to modularly designing and implementing concurrent and/or distributed systems, seeing increasing adoption in industry. But deductive verification tailored to actor programs remains underexplored; …
pdf acmKuru, Ismail, Gordon, Colin S.
European Symposium on Programming (ESOP 2019), April 2019, doi: 10.1007/978-3-030-17184-1_4
Memory management in lock-free data structures remains a major challenge in concurrent programming. Design techniques including read-copy-update (RCU) and hazard pointers provide workable solutions, and are widely used to great effect. These techniqu…
pdf springer arXivMatskevich, Sergey, Gordon, Colin S.
ACM Workshop on Natural Language for Software Engineering (NL4SE), November 2018, doi: 10.1145/3283812.3283822
Good comments help developers understand software faster and provide better maintenance. However, comments are often missing, generally inaccurate, or out of date. Many of these problems can be avoided by automatic comment generation. This paper pres…
pdf acm arXivGordon, Colin S.
Off the Beaten Track Workshop (OBT'18), January 2018
Designing a static analysis is generally a substantial undertaking, requiring significant expertise in both program analysis and the domain of interest, and significant development resources. As a result, most program analyses target properties that …
pdf url arXivGordon, Colin S., Ernst, Michael D., Grossman, Dan, Parkinson, Matthew J.
ACM Transactions on Programming Languages and Systems (TOPLAS), volume 39, number 3, July 2017, doi: 10.1145/3064850
We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The type system supports abstract and recursive objects, and is expressive e…
pdf url acm youtubeGordon, Colin S.
Proceedings of the 31st European Conference on Object-Oriented Programming (ECOOP'17), June 2017, doi: 10.4230/LIPIcs.ECOOP.2017.13
Effect systems are lightweight extensions to type systems that can verify a wide range of important properties with modest developer burden. But our general understanding of effect systems is limited primarily to systems where the order of effects is…
pdf url lipics youtube arXivChandra, Satish, Gordon, Colin S., Jeannin, Jean-Baptiste, Schlesinger, Cole , Sridharan, Manu, Tip, Frank, Choi, Young-Il
Proceedings of the 2016 ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016), November 2016, doi: 10.1145/2983990.2984017
We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The type system supports abstract and recursive objects, and is expressive e…
pdf urlAndreasen, Esben, Gordon, Colin S., Chandra, Satish, Sridharan, Manu, Tip, Frank, Sen, Koushik
Proceedings of the 30th European Conference on Object-Oriented Programming (ECOOP'16), July 2016, doi: 10.4230/LIPIcs.ECOOP.2016.1
Recent years have seen growing interest in the retrofitting of type systems onto dynamically-typed programming languages, in order to improve type safety, programmer productivity, or performance. In such cases, type system developers must strike a de…
pdfGordon, Colin S., Dietl, Werner, Ernst, Michael D., Grossman, Dan
Proceedings of the 27th European Conference on Object-Oriented Programming (ECOOP'13), July 2013, doi: 10.1007/978-3-642-39038-8_8
Most graphical user interface (GUI) libraries forbid accessing UI elements from threads other than the UI event loop thread. Violating this requirement leads to a program crash or an inconsistent UI. Unfortunately, such errors are all too common in G…
pdf urlGordon, Colin S., Ernst, Michael D., Grossman, Dan
Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'13), June 2013, doi: 10.1145/2491956.2462160
Reasoning about side effects and aliasing is the heart of verifying imperative programs. Unrestricted side effects through one reference can invalidate assumptions about an alias. We present a new type system approach to reasoning about safe assumpti…
pdf urlGordon, Colin S., Parkinson, Matthew J., Parsons, Jared, Bromfield, Aleks, Duffy, Joe
Proceedings of the 2012 ACM International Conference on Object Oriented Programming, Systems, Languages, and Applications (OOPSLA'12), October 2012, doi: 10.1145/2384616.2384619
A key challenge for concurrent programming is that side-effects (memory operations) in one thread can affect the behavior of another thread. In this paper, we present a type system to restrict the updates to memory to prevent these unintended side-ef…
pdf urlColin S. Gordon
Off the Beaten Track Workshop (OBT'12), January 2012
Software testing constitutes a substantial portion of the real world work of developing software. There has been much research aimed at partially-automating testing (random test generation, etc.). However, relatively little of it pays attention to pr…
pdf urlColin S. Gordon, Michael D. Ernst, Dan Grossman
Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'12), January 2012, doi: 10.1145/2103786.2103796
We present a technique - lock capabilities - for statically verifying that multithreaded programs with locks will not deadlock. Most previous work is built around a strict total order on all locks held simultaneously by a thread, but such an invarian…
pdf urlColin Gordon, Leo Meyerovich, Joel Weinberger, Shriram Krishnamurthi
Proceedings of the 14th International Workshop on Abstract State Machines (ASM'07), June 2007
Abstract State Machines (ASMs) offer a formalism for describing state transitions over relational structures. This makes them promising for modeling system features such as access control, especially in an environment where the policy's outcome depen…
pdf urlGordon, Colin S.
August 2014
This dissertation proposes a family of techniques for static verification of sequential and concurrent imperative programs by leveraging fine-grained characterizations of mutation. The key idea is that by attaching to each reference in a program (1) …
pdf urlColin Stebbins Gordon
June 2008
Garbage collectors are an important part of many modern language runtimes. Essentially all tools for developing and debugging programs using garbage collection assume the correctness of the collector, and therefore provide no means for detecting garb…
pdf urlLeo A. Meyerovich, Joel H. W. Weinberger, Colin S. Gordon, Shriram Krishnamurthi
number CS-06-12, November 2006
We present a model of the security policy for the Web-based Continue conference management tool. The policy model and properties are written as ASM Relational Transducers, which we extend with a module system in order to simplify the handling of conf…
pdf url