CAV 2003: 15th Computer-Aided Verification conference - Satellite Workshops
CAV 2003 Home Page

Volume 89, Number 1, 2003

PDMC 2003: 2nd International Workshop on Parallel and Distributed Model Checking
July 2003
PDMC 2003 Home Page

• 
  Lubos Brim, Orna Grumberg: Preface. 1-2
• 
  Assaf Schuster: Scalable Distributed Model Checking: Experiences, Lessons, and Expectations. 3
• 
  Martin Leucker, Rafal Somla, Michael Weber: Parallel Model Checking for LTL, CTL*, and Lµ². 4-16
• 
  Lubos Brim, Jitka Zidkova: Using Assumptions to Distribute Alternation Free Mu-Calculus Model Checking. 17-32
• 
  Pavel Krcál: Distributed Explicit Bounded LTL Model Checking. 33-50
• 
  Hemanthkumar Sivaraj, Ganesh Gopalakrishnan: Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking. 51-67
• 
  Stefan Blom, Izak van Langevelde, Bert Lisser: Compressed and Distributed File Formats for Labeled Transition Systems. 68-83
• 
  Michael D. Jones, Eric Mercer, Tonglaga Bao, Rahul Kumar, Peter Lamborn: Benchmarking Explicit State Parallel Model Checkers. 84-98
• 
  Stefan Blom, Simona Orzan: Distributed Branching Bisimulation Reduction of State Spaces. 99-113
• 
  Christophe Joubert: Distributed Model Checking: From Abstract Algorithms to Concrete Implementations. 114-127

Volume 89, Number 2, 2003

RV 2003: Third Workshop on Run-time Verification
July 2003
RV 2003 Home Page

• 
  Aloysius K. Mok: Event-Based Real-Time Monitoring. 1
• 
  Michelle L. Crane, Jürgen Dingel: Runtime Conformance Checking of Objects Using Alloy. 2-21
• 
  Alper Sen, Vijay K. Garg: Partial Order Trace Analyzer (POTA) for Distributed Programs. 22-43
• 
  Nicholas Nethercote, Julian Seward: Valgrind: A Program Supervision Framework. 44-66
• 
  Oscar Mondragon, Ann Q. Gates, Steve Roach: Prospec: Support for Elicitation and Formal Specification of Software Properties. 67-88
• 
  Clark W. Barrett, Benjamin Goldberg, Lenore D. Zuck: Run-Time Validation of Speculative Optimizations using CVC. 89-107
• 
  Feng Chen, Grigore Rosu: Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation. 108-127
• 
  Li Tan, Jesung Kim, Insup Lee: Testing and Monitoring Model-based Generated Program. 128-148
• 
  Nicholas Nethercote, Alan Mycroft: Redux: A Dynamic Dataflow Tracer. 149-170
• 
  Usa Sammapun, Raman Sharykin, Margaret DeLap, Myong Kim, Steve Zdancewic: Formalizing Java-MaC. 171-190
• 
  Liqiang Wang, Scott D. Stoller: Run-Time Analysis for Atomicity. 191-209
• 
  Kåre J. Kristoffersen, Christian Pedersen, Henrik Reif Andersen: Runtime Verification of Timed LTL using Disjunctive Normalized Equation Systems. 210-225
• 
  Koushik Sen, Grigore Rosu: Generating Optimal Monitors for Extended Regular Expressions. 226-245
• 
  Oleg Sokolsky, Mahesh Viswanathan: Preface. 246-247

Volume 89, Number 3, 2003

SoftMC 2003: Workshop on Software Model Checking
July 2003
SoftMC 2003 Home Page

• 
  Byron Cook, Scott D. Stoller, Willem Visser: SoftMC 2003: Workshop on Software Model Checking. 377
• 
  Madanlal Musuvathi, Dawson R. Engler: Some Lessons from Using Static Analysis and Software Model Checking for Bug Finding. 378-404
• 
  Dennis Dams: Comparing Abstraction Refinement Algorithms. 405-416
• 
  Sagar Chaki, Joël Ouaknine, Karen Yorav, Edmund M. Clarke: Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach. 417-432
• 
  Songtao Xia, James Hook: Experience with Abstraction-carrying Code. 433-449
• 
  Eran Yahav, Shmuel Sagiv: Automatically Verifying Concurrent Queue Algorithms. 450-463
• 
  Aysu Betin-Can, Tevfik Bultan: Interface-Based Specification and Verification of Concurrency Controllers. 464-479
• 
  Flavio Lerda, Nishant Sinha, Michael Theobald: Symbolic Model Checking of Software. 480-498
• 
  Robby, Matthew B. Dwyer, John Hatcliff, Radu Iosif: Space-Reduction Strategies for Model Checking Dynamic Software. 499-517
• 
  Cormac Flanagan, Shaz Qadeer: Transactions for Software Model Checking. 518-539

Volume 89, Number 4, 2003

• 
  Ofer Strichman, Armin Biere: Preface. 541-542
• 
  Niklas Eén, Niklas Sörensson: Temporal induction by incremental SAT solving. 543-560
• 
  Toni Jussila, Keijo Heljanko, Ilkka Niemelä: BMC via on-the-fly determinization. 561-577
• 
  P. Madhusudan, Wonhong Nam, Rajeev Alur: Symbolic computational techniques for solving games. 578-592
• 
  Zurab Khasidashvili, Ziyad Hanna: SAT-based methods for sequential hardware equivalence verification without synchronization. 593-607
• 
  Bing Li, Chao Wang, Fabio Somenzi: A satisfiability-based approach to abstraction refinement in model checking. 608-622
• 
  Gianpiero Cabodi, Sergio Nocco, Stefano Quer, Alex Kondratyev, Luciano Lavagno, Yosinori Watanabe: A BMC-formulation for the scheduling problem in highly constrained hardware Systems. 623-638