Venues / POPL /

POPL 2010

41 papers

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