| 2010 | Directed Proof Generation for Machine Code. | Aditya V. Thakur, Junghee Lim, Akash Lal, Amanda Burton, Evan Driscoll, Matt Elder, Tycho Andersen, Thomas W. Reps |
| 2010 | Learning Component Interfaces with May and Must Abstractions. | Rishabh Singh, Dimitra Giannakopoulou, Corina S. Pasareanu |
| 2010 | Global Reachability in Bounded Phase Multi-stack Pushdown Systems. | Anil Seth |
| 2010 | Constraint Solving for Program Verification: Theory and Practice by Example. | Andrey Rybalchenko |
| 2010 | There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code. | Thomas W. Reps, Junghee Lim, Aditya V. Thakur, Gogul Balakrishnan, Akash Lal |
| 2010 | An Abstraction-Refinement Approach to Verification of Artificial Neural Networks. | Luca Pulina, Armando Tacchella |
| 2010 | Jtlv: A Framework for Developing Verification Algorithms. | Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck |
| 2010 | Quantifier Elimination by Lazy Model Enumeration. | David Monniaux |
| 2010 | Memory Management in Concurrent Algorithms. | Maged M. Michael |
| 2010 | Petruchio: From Dynamic Networks to Nets. | Roland Meyer, Tim Strazny |
| 2010 | Lazy Annotation for Program Testing and Verification. | Kenneth L. McMillan |
| 2010 | PESSOA: A Tool for Embedded Controller Synthesis. | Manuel Mazo Jr., Anna Davitian, Paulo Tabuada |
| 2010 | Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems. | Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci |
| 2010 | Quantitative Information Flow: From Theory to Practice? | Pasquale Malacaria |
| 2010 | Generating Litmus Tests for Contrasting Memory Consistency Models. | Sela Mador-Haim, Rajeev Alur, Milo M. K. Martin |
| 2010 | Efficient Reachability Analysis of Bchi Pushdown Systems for Hardware/Software Co-verification. | Juncao Li, Fei Xie, Thomas Ball, Vladimir Levin |
| 2010 | Contessa: Concurrency Testing Augmented with Symbolic Analysis. | Sudipta Kundu, Malay K. Ganai, Chao Wang |
| 2010 | Comfusy: A Tool for Complete Functional Synthesis. | Viktor Kuncak, Mikal Mayer, Ruzica Piskac, Philippe Suter |
| 2010 | Termination Analysis with Compositional Transition Invariants. | Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger |
| 2010 | Dsolve: Safety Verification via Liquid Types. | Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala |
| 2010 | Dynamic Cutoff Detection in Parameterized Concurrent Programs. | Alexander Kaiser, Daniel Kroening, Thomas Wahl |
| 2010 | Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs. | Vineet Kahlon, Chao Wang |
| 2010 | Retrofitting Legacy Code for Security. | Somesh Jha |
| 2010 | Efficient Emptiness Check for Timed Bchi Automata. | Frdric Herbreteau, B. Srivathsan, Igor Walukiewicz |
| 2010 | PARAM: A Model Checker for Parametric Markov Models. | Ernst Moritz Hahn, Holger Hermanns, Bjrn Wachter, Lijun Zhang |