| 2011 | A Quantifier Elimination Algorithm for Linear Modular Equations and Disequations. Ajith K. John, Supratik Chakraborty |
| 2011 | A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification. Wei-Ngan Chin, Cristian Gherghina, Razvan Voicu, Quang Loc Le, Florin Craciun, Shengchao Qin |
| 2011 | Analyzing Unsynthesizable Specifications for High-Level Robot Behavior Using LTLMoP. Vasumathi Raman, Hadas Kress-Gazit |
| 2011 | BAP: A Binary Analysis Platform. David Brumley, Ivan Jager, Thanassis Avgerinos, Edward J. Schwartz |
| 2011 | Bug-Assist: Assisting Fault Localization in ANSI-C Programs. Manu Jose, Rupak Majumdar |
| 2011 | CPAchecker: A Tool for Configurable Software Verification. Dirk Beyer, M. Erkan Keremoglu |
| 2011 | CVC4. Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli |
| 2011 | Complete Formal Hardware Verification of Interfaces for a FlexRay-Like Bus. Christian Müller, Wolfgang J. Paul |
| 2011 | Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings Ganesh Gopalakrishnan, Shaz Qadeer |
| 2011 | Efficient Analysis of Probabilistic Programs with an Unbounded Counter. Tomás Brázdil, Stefan Kiefer, Antonín Kucera |
| 2011 | Efficient Scenario Verification for Hybrid Automata. Alessandro Cimatti, Sergio Mover, Stefano Tonetta |
| 2011 | Equality-Based Translation Validator for LLVM. Michael Stepp, Ross Tate, Sorin Lerner |
| 2011 | Existential Quantification as Incremental SAT. Jörg Brauer, Andy King, Jael Kriener |
| 2011 | FixBag: A Fixpoint Calculator for Quantified Bag Constraints. Tuan-Hung Pham, Minh-Thai Trinh, Anh-Hoang Truong, Wei-Ngan Chin |
| 2011 | Forest Automata for Verification of Heap Manipulation. Peter Habermehl, Lukás Holík, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar |
| 2011 | Formalization and Automated Verification of RESTful Behavior. Uri Klein, Kedar S. Namjoshi |
| 2011 | From Cardiac Cells to Genetic Regulatory Networks. Radu Grosu, Grégory Batt, Flavio H. Fenton, James Glimm, Colas Le Guernic, Scott A. Smolka, Ezio Bartocci |
| 2011 | Fully Symbolic Model Checking for Timed Automata. Georges Morbé, Florian Pigorsch, Christoph Scholl |
| 2011 | Getting Rid of Store-Buffers in TSO Analysis. Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato |
| 2011 | HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection. Vijay Ganesh, Adam Kiezun, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst |
| 2011 | HMC: Verifying Functional Programs Using Abstract Interpreters. Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko |
| 2011 | Interactive Synthesis of Code Snippets. Tihomir Gvero, Viktor Kuncak, Ruzica Piskac |
| 2011 | Interpolation-Based Software Verification with Wolverine. Daniel Kroening, Georg Weissenbacher |
| 2011 | KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs. Guodong Li, Indradeep Ghosh, Sreeranga P. Rajan |
| 2011 | Kratos - A Software Model Checker for SystemC. Alessandro Cimatti, Alberto Griggio, Andrea Micheli, Iman Narasamdya, Marco Roveri |
| 2011 | Language Equivalence for Probabilistic Automata. Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell |
| 2011 | Linear Completeness Thresholds for Bounded Model Checking. Daniel Kroening, Joël Ouaknine, Ofer Strichman, Thomas Wahl, James Worrell |
| 2011 | Logic and Compositional Verification of Hybrid Systems - (Invited Tutorial). André Platzer |
| 2011 | Malware Analysis with Tree Automata Inference. Domagoj Babic, Daniel Reynaud, Dawn Song |
| 2011 | Model Checking Algorithms for CTMDPs. Peter Buchholz, Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang |
| 2011 | Model Checking Recursive Programs with Numeric Data Types. Matthew Hague, Anthony Widjaja Lin |
| 2011 | Monitorability of Stochastic Dynamical Systems. A. Prasad Sistla, Milos Zefran, Yao Feng |
| 2011 | PRISM 4.0: Verification of Probabilistic Real-Time Systems. Marta Z. Kwiatkowska, Gethin Norman, David Parker |
| 2011 | Parameter Identification for Markov Models of Biochemical Reactions. Aleksandr Andreychenko, Linar Mikeev, David Spieler, Verena Wolf |
| 2011 | Practical, Low-Effort Equivalence Verification of Real Code. David A. Ramos, Dawson R. Engler |
| 2011 | Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. Kamil Dudka, Petr Peringer, Tomás Vojnar |
| 2011 | Program Analysis for Overlaid Data Structures. Oukseh Lee, Hongseok Yang, Rasmus Petersen |
| 2011 | Quantitative Synthesis for Concurrent Programs. Pavol Cerný, Krishnendu Chatterjee, Thomas A. Henzinger, Arjun Radhakrishna, Rohit Singh |
| 2011 | Relational Abstractions for Continuous and Hybrid Systems. Sriram Sankaranarayanan, Ashish Tiwari |
| 2011 | Resolution Proofs and Skolem Functions in QBF Evaluation and Applications. Valeriy Balabanov, Jie-Hong R. Jiang |
| 2011 | SLAyer: Memory Safety for Systems-Level Code. Josh Berdine, Byron Cook, Samin Ishtiaq |
| 2011 | SMT-Based Modular Analysis of Sequential Systems Code. Shuvendu K. Lahiri |
| 2011 | Simplifying Loop Invariant Generation Using Splitter Predicates. Rahul Sharma, Isil Dillig, Thomas Dillig, Alex Aiken |
| 2011 | Smoothing a Program Soundly and Robustly. Swarat Chaudhuri, Armando Solar-Lezama |
| 2011 | SpaceEx: Scalable Verification of Hybrid Systems. Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, Oded Maler |
| 2011 | Stability in Weak Memory Models. Jade Alglave, Luc Maranget |
| 2011 | State/Event-Based LTL Model Checking under Parametric Generalized Fairness. Kyungmin Bae, José Meseguer |
| 2011 | Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives. Krishnendu Chatterjee, Monika Henzinger, Manas Joglekar, Nisarg Shah |
| 2011 | Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs. Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Thomas Wahl |
| 2011 | Synthesis of Distributed Control through Knowledge Accumulation. Gal Katz, Doron A. Peled, Sven Schewe |
| 2011 | Synthesizing Biological Theories. Hillel Kugler, Cory Plock, Andy Roberts |
| 2011 | Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints. Christine Hang, Panagiotis Manolios, Vasilis Papavasileiou |
| 2011 | Synthia: Verification and Synthesis for Timed Automata. Hans-Jörg Peter, Rüdiger Ehlers, Robert Mattmüller |
| 2011 | Temporal Property Verification as a Program Analysis Task. Byron Cook, Eric Koskinen, Moshe Y. Vardi |
| 2011 | The BINCOA Framework for Binary Code Analysis. Sébastien Bardin, Philippe Herrmann, Jérôme Leroux, Olivier Ly, Renaud Tabary, Aymeric Vincent |
| 2011 | Threader: A Constraint-Based Verifier for Multi-threaded Programs. Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko |
| 2011 | Time for Statistical Model Checking of Real-Time Systems. Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Zheng Wang |
| 2011 | Using Coverage to Deploy Formal Verification in a Simulation World. Vigyan Singhal, Prashant Aggarwal |
| 2011 | Using Types for Software Verification. Ranjit Jhala |
| 2011 | Verification of Certifying Computations. Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah |