Electronic Notes in Theoretical Computer Science, Volume 89

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