| 2010 | A relational modal logic for higher-order stateful ADTs. Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal |
| 2010 | A simple, verified validator for software pipelining. Jean-Baptiste Tristan, Xavier Leroy |
| 2010 | A theory of indirection via approximation. Aquinas Hobor, Robert Dockins, Andrew W. Appel |
| 2010 | A verified compiler for an impure functional language. Adam Chlipala |
| 2010 | Abstraction-guided synthesis of synchronization. Martin T. Vechev, Eran Yahav, Greta Yorsh |
| 2010 | Automatic numeric abstractions for heap-manipulating programs. Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay |
| 2010 | Automatically generating instruction selectors using declarative machine descriptions. João Dias, Norman Ramsey |
| 2010 | Coarse-grained transactions. Eric Koskinen, Matthew J. Parkinson, Maurice Herlihy |
| 2010 | Compositional may-must program analysis: unleashing the power of alternation. Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, SaiDeep Tetali |
| 2010 | Continuity analysis of programs. Swarat Chaudhuri, Sumit Gulwani, Roberto Lublinerman |
| 2010 | Contracts made manifest. Michael Greenberg, Benjamin C. Pierce, Stephanie Weirich |
| 2010 | Counterexample-guided focus. Andreas Podelski, Thomas Wies |
| 2010 | Decision procedures for algebraic data types with abstractions. Philippe Suter, Mirco Dotta, Viktor Kuncak |
| 2010 | Dependent types and program equivalence. Limin Jia, Jianzhou Zhao, Vilhelm Sjöberg, Stephanie Weirich |
| 2010 | Dependent types from counterexamples. Tachio Terauchi |
| 2010 | Dynamically checking ownership policies in concurrent c/c++ programs. Jean-Phillipe Martin, Michael Hicks, Manuel Costa, Periklis Akritidis, Miguel Castro |
| 2010 | From Boolean to quantitative notions of correctness. Thomas A. Henzinger |
| 2010 | From program verification to program synthesis. Saurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster |
| 2010 | Generating compiler optimizations from proofs. Ross Tate, Michael Stepp, Sorin Lerner |
| 2010 | Higher-order multi-parameter tree transducers and recursion schemes for program verification. Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno |
| 2010 | Integrating typed and untyped code in a scripting language. Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, Jan Vitek |
| 2010 | Low-level liquid types. Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala |
| 2010 | Modular session types for distributed object-oriented programming. Simon J. Gay, Vasco Thudichum Vasconcelos, António Ravara, Nils Gesbert, Alexandre Z. Caldeira |
| 2010 | Modular verification of security protocol code by typing. Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon |
| 2010 | Monads in action. Andrzej Filinski |
| 2010 | Nested interpolants. Matthias Heizmann, Jochen Hoenicke, Andreas Podelski |
| 2010 | Nominal system T. Andrew M. Pitts |
| 2010 | On the verification problem for weak memory models. Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi |
| 2010 | Paralocks: role-based information flow control and beyond. Niklas Broberg, David Sands |
| 2010 | Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010 Manuel V. Hermenegildo, Jens Palsberg |
| 2010 | Program analysis via satisfiability modulo path programs. William R. Harris, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta |
| 2010 | Programming with angelic nondeterminism. Rastislav Bodík, Satish Chandra, Joel Galenson, Doug Kimelman, Nicholas Tung, Shaon Barman, Casey Rodarmor |
| 2010 | Pure subtype systems. DeLesley S. Hutchins |
| 2010 | Reconfigurable asynchronous logic automata: (RALA). Neil Gershenfeld, David Dalrymple, Kailiang Chen, Ara N. Knaian, Forrest Green, Erik D. Demaine, Scott Greenwald, Peter Schmidt-Nielsen |
| 2010 | Semantics and algorithms for data-dependent grammars. Trevor Jim, Yitzhak Mandelbaum, David Walker |
| 2010 | Sequential verification of serializability. Hagit Attiya, G. Ramalingam, Noam Rinetzky |
| 2010 | Static determination of quantitative resource usage for higher-order programs. Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, Martin Hofmann |
| 2010 | Structuring the verification of heap-manipulating programs. Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine |
| 2010 | Threesomes, with and without blame. Jeremy G. Siek, Philip Wadler |
| 2010 | Toward a verified relational database management system. J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky |
| 2010 | Type inference for datalog with complex type hierarchies. Max Schäfer, Oege de Moor |
| 2010 | Verified just-in-time compiler on x86. Magnus O. Myreen |