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

Kurt Jensen, Andreas Podelski (Eds.): 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. Lecture Notes in Computer Science 2988 Springer 2004, ISBN 3-540-21299-X

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

Last update Fri May 24 19:52:11 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page