10. TACAS 2004: Barcelona, Spain (Part of ETAPS 2004)

@proceedings{DBLP:conf/tacas/2004,
  editor    = {Kurt Jensen and
               Andreas Podelski},
  title     = {Tools and Algorithms for the Construction and Analysis of Systems,
               10th International Conference, TACAS 2004, Held as Part of the
               Joint European Conferences on Theory and Practice of Software,
               ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2988},
  year      = {2004},
  isbn      = {3-540-21299-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Theorem Proving

• Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur:
  Revisiting Positive Equality. 1-15
  
• Kenneth L. McMillan:
  An Interpolating Theorem Prover. 16-30
  
• Kavita Ravi, Fabio Somenzi:
  Minimal Assignments for Bounded Model Checking. 31-45
  

Probabilistic Model Checking

• Håkan L. S. Younes, Marta Z. Kwiatkowska, Gethin Norman, David Parker:
  Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study. 46-60
  
• Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen:
  Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes. 61-76
  
• Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga:
  Model Checking Discounted Temporal Properties. 77-92
  

Testing

• Thomas Ball, Vladimir Levin, Fei Xie:
  Automatic Creation of Environment Models via Training. 93-107
  
• Alex Groce:
  Error Explanation with Distance Metrics. 108-122
  
• Koushik Sen, Grigore Rosu, Gul Agha:
  Online Efficient Predictive Safety Analysis of Multithreaded Programs. 123-138
  

Tools

• Karsten Diethers, Michaela Huhn:
  Vooduu: Verification of Object-Oriented Designs Using UPPAAL. 139-143
  
• Carla Piazza, Enrico Pivato, Sabina Rossi:
  CoPS - Checker of Persistent Security. 144-152
  
• Heikki Virtanen, Henri Hansen, Antti Valmari, Juha Nieminen, Timo Erkkilä:
  Tampere Verification Tool. 153-157
  
• Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Masaaki Mizuno:
  SyncGen: An Aspect-Oriented Framework for Synchronization. 158-162
  
• Markus Müller-Olm, Haiseung Yoo:
  MetaGame: An Animation Tool for Model-Checking Games. 163-167
  
• Edmund M. Clarke, Daniel Kroening, Flavio Lerda:
  A Tool for Checking ANSI-C Programs. 168-176
  

Explicite State / Petri Nets

• Thomas Mailund, Michael Westergaard:
  Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method. 177-191
  
• Karsten Schmidt:
  Automated Generation of a Progress Measure for the Sweep-Line Method. 192-204
  
• Jaco Geldenhuys, Antti Valmari:
  Tarjan's Algorithm Makes On-the-Fly LTL Verification More Efficient. 205-219
  

Scheduling

• Jacob Illum Rasmussen, Kim Guldstrand Larsen, K. Subramani:
  Resource-Optimal Scheduling Using Priced Timed Automata. 220-235
  
• Pavel Krcál, Wang Yi:
  Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata. 236-250
  

Constraint Solving

• Flemming Nielson, Hanne Riis Nielson, Hongyan Sun, Mikael Buchholtz, René Rydhof Hansen, Henrik Pilegaard, Helmut Seidl:
  The Succinct Solver Suite. 251-265
  
• Nathan Linger, Tim Sheard:
  Binding-Time Analysis for MetaML via Type Inference and Constraint Solving. 266-279
  
• Zhendong Su, David Wagner:
  A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings. 280-295
  

Timed Systems

• Denis Lugiez, Peter Niebert, Sarah Zennou:
  A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata. 296-311
  
• Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, Radek Pelánek:
  Lower and Upper Bounds in Zone Based Abstractions of Timed Automata. 312-326
  
• Stefan Leue, Richard Mayr, Wei Wei:
  A Scalable Incomplete Test for the Boundedness of UML RT Models. 327-341
  
• Giorgio Delzanno, Pierre Ganty:
  Automatic Verification of Time Sensitive Cryptographic Protocols. 342-356
  

Case Studies

• A. E. Lindsey, Charles Pecheur:
  Simulation-Based Verification of Autonomous Controllers via Livingstone PathFinder. 357-371
  
• Danièle Beauquier, Tristan Crolard, Evguenia Prokofieva:
  Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic. 372-387
  

Software

• Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani:
  Refining Approximations in Software Predicate Abstraction. 388-403
  
• Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff:
  Checking Strong Specifications Using an Extensible Software Model Checking Framework. 404-420
  
• Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong:
  Applying Game Semantics to Compositional Software Modeling and Verification. 421-435
  

Temporal Logic

• Jan Friso Groote, Misa Keinänen:
  Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed Points. 436-450
  
• Arie Gurfinkel, Marsha Chechik:
  How Vacuous Is Vacuous? 451-466
  
• Rajeev Alur, Kousha Etessami, P. Madhusudan:
  A Temporal Logic of Nested Calls and Returns. 467-481
  
• Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck:
  Liveness with Incomprehensible Ranking. 482-496
  

Abstraction

• Kairong Qian, Albert Nymeyer:
  Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases. 497-511
  
• Denis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Reps, Shmuel Sagiv:
  Numeric Domains with Summarized Dimensions. 512-529
  
• Greta Yorsh, Thomas W. Reps, Shmuel Sagiv:
  Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. 530-545
  
• Sharon Shoham, Orna Grumberg:
  Monotonic Abstraction-Refinement for CTL. 546-560
  

Automata Techniques

• Bernard Boigelot, Axel Legay, Pierre Wolper:
  Omega-Regular Model Checking. 561-575
  
• Sébastien Bardin, Alain Finkel, Jérôme Leroux:
  FASTer Acceleration of Counter Automata in Practice. 576-590
  
• Orna Kupferman, Moshe Y. Vardi:
  From Complementation to Certification. 591-606