CAV 2011

60 papers

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