20. CAV 2008: Princeton, NJ, USA

Invited Talks

• James R. Larus:
  Singularity: Designing Better Software (Invited Talk). 1-2
  
• Edward W. Felten:
  Coping with Outside-the-Box Attacks. 3-4
  

Invited Tutorials

• Harry Foster:
  Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial). 5-10
  
• John Harrison:
  Theorem Proving for Verification (Invited Tutorial). 11-18
  
• Peter W. O'Hearn:
  Tutorial on Separation Logic (Invited Tutorial). 19-21
  
• Reinhard Wilhelm, Björn Wachter:
  Abstract Interpretation with Applications to Timing Validation. 22-36
  

Concurrency

• Akash Lal, Thomas W. Reps:
  Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. 37-51
  
• Azadeh Farzan, P. Madhusudan:
  Monitoring Atomicity in Concurrent Programs. 52-65
  
• Sarvani S. Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby:
  Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings. 66-79
  
• Naoki Kobayashi, Davide Sangiorgi:
  A Hybrid Type System for Lock-Freedom of Mobile Processes. 80-93
  

Memory Consistency

• Surender Baswana, Shashank K. Mehta, Vishal Powar:
  Implied Set Closure and Its Application to Memory Consistency Verification. 94-106
  
• Sebastian Burckhardt, Madanlal Musuvathi:
  Effective Program Verification for Relaxed Memory Models. 107-120
  
• Ariel Cohen, Amir Pnueli, Lenore D. Zuck:
  Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. 121-134
  

Abstraction/Refinement

• Mihaela Gheorghiu Bobaru, Corina S. Pasareanu, Dimitra Giannakopoulou:
  Automated Assume-Guarantee Reasoning by Abstraction Refinement. 135-148
  
• Ariel Cohen, Kedar S. Namjoshi:
  Local Proofs for Linear-Time Properties of Concurrent Programs. 149-161
  
• Holger Hermanns, Björn Wachter, Lijun Zhang:
  Probabilistic CEGAR. 162-175
  

Hybrid Systems

• André Platzer, Edmund M. Clarke:
  Computing Differential Invariants of Hybrid Systems as Fixedpoints. 176-189
  
• Sumit Gulwani, Ashish Tiwari:
  Constraint-Based Approach for Analysis of Hybrid Systems. 190-203
  

Tools - Dynamic Verification

• Ambar A. Gadkari, Anand Yeolekar, J. Suresh, S. Ramesh, Swarup Mohalik, K. C. Shashidhar:
  AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems. 204-208
  
• Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith:
  FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement. 209-213
  

Modeling and Specification Formalisms

• Salil Joshi, Barbara König:
  Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems. 214-226
  
• Deepak D'Souza, Madhu Gopinathan:
  Conflict-Tolerant Features. 227-239
  
• Rajeev Alur, Aditya Kanade, Gera Weiss:
  Ranking Automata and Games for Prioritized Requirements. 240-253
  

Decision Procedures

• Himanshu Jain, Edmund M. Clarke, Orna Grumberg:
  Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. 254-267
  
• Ruzica Piskac, Viktor Kuncak:
  Linear Arithmetic with Stars. 268-280
  
• Andy King, Harald Søndergaard:
  Inferring Congruence Equations Using SAT. 281-293
  

Tools - Decision Procedures

• Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
  The Barcelogic SMT Solver. 294-298
  
• Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani:
  The MathSAT 4SMT Solver. 299-303
  
• Dirk Beyer, Damien Zufferey, Rupak Majumdar:
  CSIsat: Interpolation for LA+EUF. 304-308
  
• Laura I. Meikle, Jacques D. Fleuriot:
  Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B. 309-313
  

Program Verification

• Andreas Podelski, Andrey Rybalchenko, Thomas Wies:
  Heap Assumptions on Demand. 314-327
  
• Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv:
  Proving Conditional Termination. 328-340
  
• Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ahmed Rezine:
  Monotonic Abstraction for Programs with Dynamic Memory Heaps. 341-354
  
• Huu Hai Nguyen, Wei-Ngan Chin:
  Enhancing Program Verification with Lemmas. 355-369
  

Program and Shape Analysis

• Bhargav S. Gulavani, Sumit Gulwani:
  A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis. 370-384
  
• Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn:
  Scalable Shape Analysis for Systems Code. 385-398
  
• Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv:
  Thread Quantification for Concurrent Shape Analysis. 399-413
  

Tools - Security and Program Analysis

• Cas J. F. Cremers:
  The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. 414-418
  
• Michael Backes, Stefan Lorenz, Matteo Maffei, Kim Pecina:
  The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis. 419-422
  
• Johannes Kinder, Helmut Veith:
  Jakstab: A Static Analysis Platform for Binaries. 423-427
  
• Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay:
  THOR: A Tool for Reasoning about Shape and Arithmetic. 428-432
  

Hardware Verification I

• Cindy Eisner, Amir Nahir, Karen Yorav:
  Functional Verification of Power Gated Designs by Compositional Reasoning. 433-445
  
• Per Bjesse:
  A Practical Approach to Word Level Model Checking of Industrial Netlists. 446-458
  

Hardware Verification II

• Sudipta Kundu, Sorin Lerner, Rajesh Gupta:
  Validating High-Level Synthesis. 459-472
  
• Oliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, Gert-Martin Greuel:
  An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths. 473-486
  
• Hyondeuk Kim, HoonSang Jin, Kavita Ravi, Petr Spacek, John Pierce, Robert P. Kurshan, Fabio Somenzi:
  Application of Formal Word-Level Analysis to Constrained Random Simulation. 487-490
  

Model Checking

• Sujatha Kashyap, Vijay K. Garg:
  Producing Short Counterexamples Using "Crucial Events". 491-503
  
• Peter Niebert, Doron Peled, Amir Pnueli:
  Discriminative Model Checking. 504-516
  

Space Efficient Algorithms

• Rob J. van Glabbeek, Bas Ploeger:
  Correcting a Space-Efficient Simulation Algorithm. 517-529
  
• Stefan Edelkamp, Peter Sanders, Pavel Simecek:
  Semi-external LTL Model Checking. 530-542
  

Tools - Model Checking

• Simon J. Gay, Rajagopal Nagarajan, Nikolaos Papanikolaou:
  QMC: A Model Checker for Quantum Systems. 543-547
  
• Axel Legay:
  T(O)RMC: A Tool for (omega)-Regular Model Checking. 548-551
  
• Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel, Andreas Podelski:
  Faster Than Uppaal? 552-555
  

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