| 2010 | A Dash of Fairness for Compositional Reasoning. Ariel Cohen, Kedar S. Namjoshi, Yaniv Sa'ar |
| 2010 | A Logical Product Approach to Zonotope Intersection. Khalil Ghorbal, Eric Goubault, Sylvie Putot |
| 2010 | A Model Checker for AADL. Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, Ralf Wimmer |
| 2010 | A NuSMV Extension for Graded-CTL Model Checking. Alessandro Ferrante, Maurizio Memoli, Margherita Napoli, Mimmo Parente, Francesco Sorrentino |
| 2010 | ABC: An Academic Industrial-Strength Verification Tool. Robert K. Brayton, Alan Mishchenko |
| 2010 | Abstract Analysis of Symbolic Executions. Aws Albarghouthi, Arie Gurfinkel, Ou Wei, Marsha Chechik |
| 2010 | Achieving Distributed Control through Model Checking. Susanne Graf, Doron A. Peled, Sophie Quinton |
| 2010 | An Abstraction-Refinement Approach to Verification of Artificial Neural Networks. Luca Pulina, Armando Tacchella |
| 2010 | Automated Assume-Guarantee Reasoning through Implicit Learning. Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang |
| 2010 | Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics. Satrajit Chatterjee, Michael Kishinevsky |
| 2010 | Automatically Proving Linearizability. Viktor Vafeiadis |
| 2010 | Bounded Underapproximations. Pierre Ganty, Rupak Majumdar, Benjamin Monmege |
| 2010 | Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems. Alexandre Donzé |
| 2010 | Comfusy: A Tool for Complete Functional Synthesis. Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter |
| 2010 | Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings Tayssir Touili, Byron Cook, Paul B. Jackson |
| 2010 | Constraint Solving for Program Verification: Theory and Practice by Example. Andrey Rybalchenko |
| 2010 | Contessa: Concurrency Testing Augmented with Symbolic Analysis. Sudipta Kundu, Malay K. Ganai, Chao Wang |
| 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 | 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 | Efficient Emptiness Check for Timed Büchi Automata. Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz |
| 2010 | Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification. Juncao Li, Fei Xie, Thomas Ball, Vladimir Levin |
| 2010 | Fast Acceleration of Ultimately Periodic Relations. Marius Bozga, Radu Iosif, Filip Konecný |
| 2010 | Fences in Weak Memory Models. Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell |
| 2010 | Generating Litmus Tests for Contrasting Memory Consistency Models. Sela Mador-Haim, Rajeev Alur, Milo M. K. Martin |
| 2010 | Gist: A Solver for Probabilistic Games. Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Arjun Radhakrishna |
| 2010 | Global Reachability in Bounded Phase Multi-stack Pushdown Systems. Anil Seth |
| 2010 | Invariant Synthesis for Programs Manipulating Lists with Unbounded Data. Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Ahmed Rezine, Mihaela Sighireanu |
| 2010 | Jtlv: A Framework for Developing Verification Algorithms. Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck |
| 2010 | LTSmin: Distributed and Symbolic Reachability. Stefan Blom, Jaco van de Pol, Michael Weber |
| 2010 | Lazy Annotation for Program Testing and Verification. Kenneth L. McMillan |
| 2010 | Learning Component Interfaces with May and Must Abstractions. Rishabh Singh, Dimitra Giannakopoulou, Corina S. Pasareanu |
| 2010 | Local Verification of Global Invariants in Concurrent Programs. Ernie Cohen, Michal Moskal, Wolfram Schulte, Stephan Tobies |
| 2010 | Measuring and Synthesizing Systems in Probabilistic Environments. Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh |
| 2010 | Memory Management in Concurrent Algorithms. Maged M. Michael |
| 2010 | Merit: An Interpolating Model-Checker. Nicolas Caniart |
| 2010 | Model Checking of Linearizability of Concurrent List Implementations. Pavol Cerný, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, Rajeev Alur |
| 2010 | Model-Checking Parameterized Concurrent Programs Using Linear Interfaces. Salvatore La Torre, P. Madhusudan, Gennaro Parlato |
| 2010 | On Array Theory of Bounded Elements. Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu |
| 2010 | PARAM: A Model Checker for Parametric Markov Models. Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang |
| 2010 | PESSOA: A Tool for Embedded Controller Synthesis. Manuel Mazo Jr., Anna Davitian, Paulo Tabuada |
| 2010 | Petruchio: From Dynamic Networks to Nets. Roland Meyer, Tim Strazny |
| 2010 | Policy Monitoring in First-Order Temporal Logic. David A. Basin, Felix Klaedtke, Samuel Müller |
| 2010 | Quantifier Elimination by Lazy Model Enumeration. David Monniaux |
| 2010 | Quantitative Information Flow: From Theory to Practice? Pasquale Malacaria |
| 2010 | RATSY - A New Requirements Analysis Tool with Synthesis. Roderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Könighofer, Marco Roveri, Viktor Schuppan, Richard Seeber |
| 2010 | Retrofitting Legacy Code for Security. Somesh Jha |
| 2010 | Robustness in the Presence of Liveness. Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann |
| 2010 | SPLIT: A Compositional LTL Verifier. Ariel Cohen, Kedar S. Namjoshi, Yaniv Sa'ar |
| 2010 | Safety Verification for Probabilistic Hybrid Systems. Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, Ernst Moritz Hahn |
| 2010 | Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing. Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukás Holík, Chih-Duo Hong, Richard Mayr, Tomás Vojnar |
| 2010 | Symbolic Bounded Synthesis. Rüdiger Ehlers |
| 2010 | Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems. Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci |
| 2010 | Termination Analysis with Compositional Transition Invariants. Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger |
| 2010 | The Static Driver Verifier Research Platform. Thomas Ball, Ella Bounimova, Vladimir Levin, Rahul Kumar, Jakob Lichtenberg |
| 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 | Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs. Vineet Kahlon, Chao Wang |
| 2010 | Verifying Low-Level Implementations of High-Level Datatypes. Christopher L. Conway, Clark W. Barrett |
| 2010 | libalf: The Automata Learning Framework. Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker, Daniel Neider, David R. Piegdon |