22. CAV 2011: Snowbird, UT, USA

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

Last update Tue May 22 23:23:22 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page