


default search action
23rd CAV 2011: Snowbird, UT, USA
- Ganesh Gopalakrishnan, Shaz Qadeer:

Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Lecture Notes in Computer Science 6806, Springer 2011, ISBN 978-3-642-22109-5 - 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 - Aleksandr 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 W. 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 S. 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 A. 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 J. 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

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














